summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Expressions.ml1
-rw-r--r--src/ExtractToFStar.ml8
-rw-r--r--src/FunsAnalysis.ml3
-rw-r--r--src/InterpreterExpressions.ml9
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