diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Extract.ml | 11 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 24 |
2 files changed, 28 insertions, 7 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index ac81d6f3..b842aea1 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -3,7 +3,6 @@ the formatter everywhere... *) -open Utils open Pure open PureUtils open TranslateCore @@ -61,6 +60,11 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string = | Le -> "le" | Ge -> "ge" | Gt -> "gt" + | BitXor -> "xor" + | BitAnd -> "and" + | BitOr -> "or" + | Shl -> "lsl" + | Shr -> "asr" (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *) | _ -> raise (Failure "Unreachable") in (* Remark: the Lean case is actually not used *) @@ -498,14 +502,13 @@ let extract_binop (extract_expr : bool -> texpression -> unit) F.pp_print_string fmt binop; F.pp_print_space fmt (); extract_expr false arg1 - | _, (Lt | Le | Ge | Gt | Div | Rem | Add | Sub | Mul) -> + | _ -> let binop = named_binop_name binop int_ty in F.pp_print_string fmt binop; F.pp_print_space fmt (); extract_expr true arg0; F.pp_print_space fmt (); - extract_expr true arg1 - | _, (BitXor | BitAnd | BitOr | Shl | Shr) -> raise Unimplemented); + extract_expr true arg1); if inside then F.pp_print_string fmt ")" let type_decl_kind_to_qualif (kind : decl_kind) diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f4406653..f8aa06dc 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -58,6 +58,24 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) let can_diverge = ref false in let is_rec = ref false in + (* We have some specialized knowledge of some library functions; we don't + have any more custom treatment than this, and these functions can be modeled + suitably in Primitives.fst, rather than special-casing for them all the + way. *) + let module M = struct type opaque_info = { fallible: bool; stateful: bool } end in + let open M in + let opaque_info (f: fun_decl) = + match f.name with + | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "wrapping_add" ] + | [ Ident "core"; Ident "num"; Ident "u32"; _; Ident "rotate_left" ] -> + { fallible = false; stateful = false } + | _ -> + (* Opaque function: we consider they fail by default *) + { fallible = true; stateful = true } + in + + (* JP: Why not use a reduce visitor here with a tuple of the values to be + computed? *) let visit_fun (f : fun_decl) : unit = let obj = object (self) @@ -108,9 +126,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) assert ((not f.is_global_decl_body) || not !stateful); match f.body with | None -> - (* Opaque function: we consider they fail by default *) - obj#may_fail true; - stateful := (not f.is_global_decl_body) && use_state + let info = opaque_info f in + obj#may_fail info.fallible; + stateful := (not f.is_global_decl_body) && use_state && info.stateful | Some body -> obj#visit_statement () body.body in List.iter visit_fun d; |