diff options
| -rw-r--r-- | src/Expressions.ml | 1 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 8 | ||||
| -rw-r--r-- | src/FunsAnalysis.ml | 3 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 9 |
4 files changed, 12 insertions, 9 deletions
diff --git a/src/Expressions.ml b/src/Expressions.ml index 6645a77f..bf06dd1e 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -72,7 +72,6 @@ let all_binops = Shr; ] -(* TODO: symplify the operand constant values *) type operand = | Copy of place | Move of place diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 20b06bfa..5b39b0b7 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -26,7 +26,7 @@ type type_decl_qualif = *) type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal -let fun_decl_qualif_name (qualif : fun_decl_qualif) : string = +let fun_decl_qualif_keyword (qualif : fun_decl_qualif) : string = match qualif with | Let -> "let" | LetRec -> "let rec" @@ -1368,7 +1368,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hovbox fmt ctx.indent_incr; (* > "let FUN_NAME" *) let is_opaque = Option.is_none def.body in - let qualif = fun_decl_qualif_name qualif in + let qualif = fun_decl_qualif_keyword qualif in F.pp_print_string fmt (qualif ^ " " ^ def_name); F.pp_print_space fmt (); (* Open a box for "(PARAMS) : EFFECT =" *) @@ -1498,7 +1498,7 @@ let extract_global_definition (ctx : extraction_ctx) (fmt : F.formatter) (* Open "QUALIF NAME : TYPE =" box (depth=1) *) F.pp_open_hovbox fmt ctx.indent_incr; (* Print "QUALIF NAME " *) - F.pp_print_string fmt (fun_decl_qualif_name qualif ^ " " ^ name); + F.pp_print_string fmt (fun_decl_qualif_keyword qualif ^ " " ^ name); F.pp_print_space fmt (); (* Open ": TYPE =" box (depth=2) *) @@ -1558,7 +1558,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) assert (List.length def.signature.type_params = 0); assert (not def.signature.info.effect_info.can_fail); - (* Add a break then the corresponding Rust definition *) + (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; F.pp_print_string fmt ("(** [" ^ Print.fun_name_to_string def.basename ^ "] *)"); F.pp_print_space fmt (); diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml index 5a623450..b1b8ccc2 100644 --- a/src/FunsAnalysis.ml +++ b/src/FunsAnalysis.ml @@ -58,6 +58,8 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) method may_fail b = (* The fail flag is disabled for globals : the global body is * normalised into its declaration, which is always successful. + * (we check that it is successful in the extracted code: if it is + * not, it leads to a type-checking error in the generated files) *) if f.is_global then () else can_fail := !can_fail || b @@ -96,6 +98,7 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t) super#visit_Loop env loop end in + assert (not f.is_global || not use_state); (match f.body with | None -> (* Opaque function *) diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 04ad1b3c..4598895e 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -110,13 +110,13 @@ let access_rplace_reorganize (config : C.config) (expand_prim_copy : bool) ctx (** Convert an operand constant operand value to a typed value *) -let typecheck_constant_value (ty : T.ety) +let constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value = (* Check the type while converting - we actually need some information * contained in the type *) log#ldebug (lazy - ("typecheck_constant_value:" ^ "\n- cv: " + ("constant_to_typed_value:" ^ "\n- cv: " ^ PV.constant_value_to_string cv)); match (ty, cv) with (* Scalar, boolean... *) @@ -175,7 +175,8 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) : fun cf ctx -> match op with | Expressions.Constant (ty, cv) -> - typecheck_constant_value ty cv |> ignore; + (* No need to reorganize the context *) + constant_to_typed_value ty cv |> ignore; cf ctx | Expressions.Copy p -> (* Access the value *) @@ -203,7 +204,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand) ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Evaluate *) match op with - | Expressions.Constant (ty, cv) -> cf (typecheck_constant_value ty cv) ctx + | Expressions.Constant (ty, cv) -> cf (constant_to_typed_value ty cv) ctx | Expressions.Copy p -> (* Access the value *) let access = Read in |