summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Contexts.ml73
-rw-r--r--compiler/Interpreter.ml20
-rw-r--r--compiler/InterpreterBorrows.ml10
-rw-r--r--compiler/InterpreterExpansion.ml147
-rw-r--r--compiler/InterpreterExpressions.ml94
-rw-r--r--compiler/InterpreterLoopsFixedPoint.ml4
-rw-r--r--compiler/InterpreterPaths.ml12
-rw-r--r--compiler/InterpreterStatements.ml46
-rw-r--r--compiler/Main.ml2
-rw-r--r--compiler/SynthesizeSymbolic.ml35
-rw-r--r--compiler/Translate.ml6
11 files changed, 226 insertions, 223 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 2563bd9d..6cdae078 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -5,6 +5,7 @@ open LlbcAst
open LlbcAstUtils
open ValuesUtils
open Identifiers
+open Errors
module L = Logging
(** The [Id] module for dummy variables.
@@ -285,7 +286,7 @@ let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
ConstGenericVarId.nth ctx.const_generic_vars vid
(** Lookup a variable in the current frame *)
-let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
+let env_lookup_var (meta : Meta.meta) (env : env) (vid : VarId.id) : var_binder * typed_value =
(* We take care to stop at the end of current frame: different variables
in different frames can have the same id!
*)
@@ -296,12 +297,12 @@ let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
| EBinding (BVar var, v) :: env' ->
if var.index = vid then (var, v) else lookup env'
| (EBinding (BDummy _, _) | EAbs _) :: env' -> lookup env'
- | EFrame :: _ -> raise (Failure "End of frame")
+ | EFrame :: _ -> craise meta "End of frame"
in
lookup env
-let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder =
- fst (env_lookup_var ctx.env vid)
+let ctx_lookup_var_binder (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) : var_binder =
+ fst (env_lookup_var meta ctx.env vid)
let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
TypeDeclId.Map.find tid ctx.type_ctx.type_decls
@@ -320,12 +321,12 @@ let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
TraitImplId.Map.find id ctx.trait_impls_ctx.trait_impls
(** Retrieve a variable's value in the current frame *)
-let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
- snd (env_lookup_var env vid)
+let env_lookup_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) : typed_value =
+ snd (env_lookup_var meta env vid)
(** Retrieve a variable's value in an evaluation context *)
-let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
- env_lookup_var_value ctx.env vid
+let ctx_lookup_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) : typed_value =
+ env_lookup_var_value meta ctx.env vid
(** Retrieve a const generic value in an evaluation context *)
let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
@@ -337,18 +338,18 @@ let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
This is a helper function: it can break invariants and doesn't perform
any check.
*)
-let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
+let env_update_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) (nv : typed_value) : env =
(* We take care to stop at the end of current frame: different variables
in different frames can have the same id!
*)
let rec update env =
match env with
- | [] -> raise (Failure "Unexpected")
+ | [] -> craise meta "Unexpected"
| EBinding ((BVar b as var), v) :: env' ->
if b.index = vid then EBinding (var, nv) :: env'
else EBinding (var, v) :: update env'
| ((EBinding (BDummy _, _) | EAbs _) as ee) :: env' -> ee :: update env'
- | EFrame :: _ -> raise (Failure "End of frame")
+ | EFrame :: _ -> craise meta "End of frame"
in
update env
@@ -360,17 +361,17 @@ let var_to_binder (var : var) : var_binder =
This is a helper function: it can break invariants and doesn't perform
any check.
*)
-let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
+let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
eval_ctx =
- { ctx with env = env_update_var_value ctx.env vid nv }
+ { ctx with env = env_update_var_value meta ctx.env vid nv }
(** Push a variable in the context's environment.
Checks that the pushed variable and its value have the same type (this
is important).
*)
-let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
- assert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty);
+let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
+ cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "Pushed variables and their values do not have the same type TODO: Error message";
let bv = var_to_binder var in
{ ctx with env = EBinding (BVar bv, v) :: ctx.env }
@@ -379,7 +380,7 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
Checks that the pushed variables and their values have the same type (this
is important).
*)
-let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
+let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
=
log#ldebug
(lazy
@@ -390,11 +391,11 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
(* We can unfortunately not use Print because it depends on Contexts... *)
show_var var ^ " -> " ^ show_typed_value value)
vars)));
- assert (
+ cassert (
List.for_all
(fun (var, (value : typed_value)) ->
TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
- vars);
+ vars) meta "Pushed variables and their values do not have the same type TODO: Error message";
let vars =
List.map
(fun (var, value) -> EBinding (BVar (var_to_binder var), value))
@@ -416,11 +417,11 @@ let ctx_push_fresh_dummy_vars (ctx : eval_ctx) (vl : typed_value list) :
List.fold_left (fun ctx v -> ctx_push_fresh_dummy_var ctx v) ctx vl
(** Remove a dummy variable from a context's environment. *)
-let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
+let ctx_remove_dummy_var meta (ctx : eval_ctx) (vid : DummyVarId.id) :
eval_ctx * typed_value =
let rec remove_var (env : env) : env * typed_value =
match env with
- | [] -> raise (Failure "Could not lookup a dummy variable")
+ | [] -> craise meta "Could not lookup a dummy variable"
| EBinding (BDummy vid', v) :: env when vid' = vid -> (env, v)
| ee :: env ->
let env, v = remove_var env in
@@ -430,10 +431,10 @@ let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
({ ctx with env }, v)
(** Lookup a dummy variable in a context's environment. *)
-let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
+let ctx_lookup_dummy_var (meta : Meta.meta) (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
let rec lookup_var (env : env) : typed_value =
match env with
- | [] -> raise (Failure "Could not lookup a dummy variable")
+ | [] -> craise meta "Could not lookup a dummy variable"
| EBinding (BDummy vid', v) :: _env when vid' = vid -> v
| _ :: env -> lookup_var env
in
@@ -449,13 +450,13 @@ let erase_regions (ty : ty) : ty =
v#visit_ty () ty
(** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
-let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
- ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
+let ctx_push_uninitialized_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) : eval_ctx =
+ ctx_push_var meta ctx var (mk_bottom (erase_regions var.var_ty))
(** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
-let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
+let ctx_push_uninitialized_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : var list) : eval_ctx =
let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
- ctx_push_vars ctx vars
+ ctx_push_vars meta ctx vars
let env_find_abs (env : env) (pred : abs -> bool) : abs option =
let rec lookup env =
@@ -474,10 +475,10 @@ let env_lookup_abs_opt (env : env) (abs_id : AbstractionId.id) : abs option =
this abstraction (for instance, remove the abs id from all the parent sets
of all the other abstractions).
*)
-let env_remove_abs (env : env) (abs_id : AbstractionId.id) : env * abs option =
+let env_remove_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) : env * abs option =
let rec remove (env : env) : env * abs option =
match env with
- | [] -> raise (Failure "Unreachable")
+ | [] -> craise meta "Unreachable"
| EFrame :: _ -> (env, None)
| EBinding (bv, v) :: env ->
let env, abs_opt = remove env in
@@ -499,11 +500,11 @@ let env_remove_abs (env : env) (abs_id : AbstractionId.id) : env * abs option =
we also substitute the abstraction id wherever it is used (i.e., in the
parent sets of the other abstractions).
*)
-let env_subst_abs (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
+let env_subst_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
env * abs option =
let rec update (env : env) : env * abs option =
match env with
- | [] -> raise (Failure "Unreachable")
+ | [] -> craise meta "Unreachable"
| EFrame :: _ -> (* We're done *) (env, None)
| EBinding (bv, v) :: env ->
let env, opt_abs = update env in
@@ -535,22 +536,22 @@ let ctx_find_abs (ctx : eval_ctx) (p : abs -> bool) : abs option =
env_find_abs ctx.env p
(** See the comments for {!env_remove_abs} *)
-let ctx_remove_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) :
+let ctx_remove_abs (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id) :
eval_ctx * abs option =
- let env, abs = env_remove_abs ctx.env abs_id in
+ let env, abs = env_remove_abs meta ctx.env abs_id in
({ ctx with env }, abs)
(** See the comments for {!env_subst_abs} *)
-let ctx_subst_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
+let ctx_subst_abs (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
eval_ctx * abs option =
- let env, abs_opt = env_subst_abs ctx.env abs_id nabs in
+ let env, abs_opt = env_subst_abs meta ctx.env abs_id nabs in
({ ctx with env }, abs_opt)
-let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
+let ctx_set_abs_can_end (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id)
(can_end : bool) : eval_ctx =
let abs = ctx_lookup_abs ctx abs_id in
let abs = { abs with can_end } in
- fst (ctx_subst_abs ctx abs_id abs)
+ fst (ctx_subst_abs meta ctx abs_id abs)
let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
let decl_group = TypeDeclId.Map.find id ctx.type_ctx.type_decls_groups in
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index ccae4588..961a64a4 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -173,7 +173,7 @@ let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
- the list of symbolic values introduced for the input values
- the instantiated function signature
*)
-let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
+let initialize_symbolic_context_for_fun (meta : Meta.meta) (ctx : decls_ctx) (fdef : fun_decl) :
eval_ctx * symbolic_value list * inst_fun_sig =
(* The abstractions are not initialized the same way as for function
* calls: they contain *loan* projectors, because they "provide" us
@@ -232,12 +232,12 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
Collections.List.split_at (List.tl body.locals) body.arg_count
in
(* Push the return variable (initialized with ⊥) *)
- let ctx = ctx_push_uninitialized_var ctx ret_var in
+ let ctx = ctx_push_uninitialized_var meta ctx ret_var in
(* Push the input variables (initialized with symbolic values) *)
let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
- let ctx = ctx_push_vars ctx (List.combine input_vars input_values) in
+ let ctx = ctx_push_vars meta ctx (List.combine input_vars input_values) in
(* Push the remaining local variables (initialized with ⊥) *)
- let ctx = ctx_push_uninitialized_vars ctx local_vars in
+ let ctx = ctx_push_uninitialized_vars meta ctx local_vars in
(* Return *)
(ctx, input_svs, inst_sg)
@@ -468,7 +468,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
for the synthesis)
- the symbolic AST generated by the symbolic execution
*)
-let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
+let evaluate_function_symbolic (meta : Meta.meta) (synthesize : bool) (ctx : decls_ctx)
(fdef : fun_decl) : symbolic_value list * SA.expression option =
(* Debug *)
let name_to_string () =
@@ -479,7 +479,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ()));
(* Create the evaluation context *)
- let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in
+ let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun meta ctx fdef in
let regions_hierarchy =
FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
@@ -612,7 +612,7 @@ module Test = struct
(** Test a unit function (taking no arguments) by evaluating it in an empty
environment.
*)
- let test_unit_function (crate : crate) (decls_ctx : decls_ctx)
+ let test_unit_function (meta : Meta.meta) (crate : crate) (decls_ctx : decls_ctx)
(fid : FunDeclId.id) : unit =
(* Retrieve the function declaration *)
let fdef = FunDeclId.Map.find fid crate.fun_decls in
@@ -634,7 +634,7 @@ module Test = struct
let ctx = initialize_eval_ctx decls_ctx [] [] [] in
(* Insert the (uninitialized) local variables *)
- let ctx = ctx_push_uninitialized_vars ctx body.locals in
+ let ctx = ctx_push_uninitialized_vars meta ctx body.locals in
(* Create the continuation to check the function's result *)
let config = mk_config ConcreteMode in
@@ -665,7 +665,7 @@ module Test = struct
&& def.signature.inputs = []
(** Test all the unit functions in a list of function definitions *)
- let test_unit_functions (crate : crate) : unit =
+ let test_unit_functions (meta : Meta.meta) (crate : crate) : unit =
let unit_funs =
FunDeclId.Map.filter
(fun _ -> fun_decl_is_transparent_unit)
@@ -673,7 +673,7 @@ module Test = struct
in
let decls_ctx = compute_contexts crate in
let test_unit_fun _ (def : fun_decl) : unit =
- test_unit_function crate decls_ctx def.def_id
+ test_unit_function meta crate decls_ctx def.def_id
in
FunDeclId.Map.iter test_unit_fun unit_funs
end
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index ae251fbf..e37a67b7 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1030,7 +1030,7 @@ and end_abstraction_aux (meta : Meta.meta) (config : config) (chain : borrow_or_
(* Remove all the references to the id of the current abstraction, and remove
* the abstraction itself.
* **Rk.**: this is where we synthesize the updated symbolic AST *)
- let cc = comp cc (end_abstraction_remove_from_context config abs_id) in
+ let cc = comp cc (end_abstraction_remove_from_context meta config abs_id) in
(* Debugging *)
let cc =
@@ -1273,10 +1273,10 @@ and end_abstraction_borrows (meta : Meta.meta) (config : config) (chain : borrow
end_abstraction_borrows meta config chain abs_id cf ctx
(** Remove an abstraction from the context, as well as all its references *)
-and end_abstraction_remove_from_context (_config : config)
+and end_abstraction_remove_from_context (meta : Meta.meta) (_config : config)
(abs_id : AbstractionId.id) : cm_fun =
fun cf ctx ->
- let ctx, abs = ctx_remove_abs ctx abs_id in
+ let ctx, abs = ctx_remove_abs meta ctx abs_id in
let abs = Option.get abs in
(* Apply the continuation *)
let expr = cf ctx in
@@ -2502,8 +2502,8 @@ let merge_into_abstraction (meta : Meta.meta) (abs_kind : abs_kind) (can_end : b
(* Update the environment: replace the abstraction 1 with the result of the merge,
remove the abstraction 0 *)
- let ctx = fst (ctx_subst_abs ctx abs_id1 nabs) in
- let ctx = fst (ctx_remove_abs ctx abs_id0) in
+ let ctx = fst (ctx_subst_abs meta ctx abs_id1 nabs) in
+ let ctx = fst (ctx_remove_abs meta ctx abs_id0) in
(* Merge all the regions from the abstraction into one (the first - i.e., the
one with the smallest id). Note that we need to do this in the whole
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index e489ddc3..0a5a289e 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -13,6 +13,7 @@ open ValuesUtils
open InterpreterUtils
open InterpreterProjectors
open Print.EvalCtx
+open Errors
module S = SynthesizeSymbolic
(** The local logger *)
@@ -47,7 +48,7 @@ type proj_kind = LoanProj | BorrowProj
Note that 2. and 3. may have a little bit of duplicated code, but hopefully
it would make things clearer.
*)
-let apply_symbolic_expansion_to_target_avalues (config : config)
+let apply_symbolic_expansion_to_target_avalues (meta : Meta.meta) (config : config)
(allow_reborrows : bool) (proj_kind : proj_kind)
(original_sv : symbolic_value) (expansion : symbolic_expansion)
(ctx : eval_ctx) : eval_ctx =
@@ -65,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
(** When visiting an abstraction, we remember the regions it owns to be
able to properly reduce projectors when expanding symbolic values *)
method! visit_abs current_abs abs =
- assert (Option.is_none current_abs);
+ cassert (Option.is_none current_abs) meta "T";
let current_abs = Some abs in
super#visit_abs current_abs abs
@@ -77,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
method! visit_aproj current_abs aproj =
(match aproj with
| AProjLoans (sv, _) | AProjBorrows (sv, _) ->
- assert (not (same_symbolic_id sv original_sv))
+ cassert (not (same_symbolic_id sv original_sv)) meta "T"
| AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
super#visit_aproj current_abs aproj
@@ -97,7 +98,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
(* Check if this is the symbolic value we are looking for *)
if same_symbolic_id sv original_sv then (
(* There mustn't be any given back values *)
- assert (given_back = []);
+ cassert (given_back = []) meta "T";
(* Apply the projector *)
let projected_value =
apply_proj_loans_on_symbolic_expansion proj_regions
@@ -145,11 +146,11 @@ let apply_symbolic_expansion_to_target_avalues (config : config)
(** Auxiliary function.
Apply a symbolic expansion to avalues in a context.
*)
-let apply_symbolic_expansion_to_avalues (config : config)
+let apply_symbolic_expansion_to_avalues (meta : Meta.meta) (config : config)
(allow_reborrows : bool) (original_sv : symbolic_value)
(expansion : symbolic_expansion) (ctx : eval_ctx) : eval_ctx =
let apply_expansion proj_kind ctx =
- apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
+ apply_symbolic_expansion_to_target_avalues meta config allow_reborrows proj_kind
original_sv expansion ctx
in
(* First target the loan projectors, then the borrow projectors *)
@@ -162,12 +163,12 @@ let apply_symbolic_expansion_to_avalues (config : config)
Simply replace the symbolic values (*not avalues*) in the context with
a given value. Will break invariants if not used properly.
*)
-let replace_symbolic_values (at_most_once : bool) (original_sv : symbolic_value)
+let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_sv : symbolic_value)
(nv : value) (ctx : eval_ctx) : eval_ctx =
(* Count *)
let replaced = ref false in
let replace () =
- if at_most_once then assert (not !replaced);
+ if at_most_once then cassert (not !replaced) meta "T";
replaced := true;
nv
in
@@ -186,16 +187,16 @@ let replace_symbolic_values (at_most_once : bool) (original_sv : symbolic_value)
(* Return *)
ctx
-let apply_symbolic_expansion_non_borrow (config : config)
+let apply_symbolic_expansion_non_borrow (meta : Meta.meta) (config : config)
(original_sv : symbolic_value) (expansion : symbolic_expansion)
(ctx : eval_ctx) : eval_ctx =
(* Apply the expansion to non-abstraction values *)
let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
let at_most_once = false in
- let ctx = replace_symbolic_values at_most_once original_sv nv.value ctx in
+ let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
(* Apply the expansion to abstraction values *)
let allow_reborrows = false in
- apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+ apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
expansion ctx
(** Compute the expansion of a non-assumed (i.e.: not [Box], etc.)
@@ -208,13 +209,13 @@ let apply_symbolic_expansion_non_borrow (config : config)
[expand_enumerations] controls the expansion of enumerations: if false, it
doesn't allow the expansion of enumerations *containing several variants*.
*)
-let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
+let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_enumerations : bool)
(def_id : TypeDeclId.id) (generics : generic_args) (ctx : eval_ctx) :
symbolic_expansion list =
(* Lookup the definition and check if it is an enumeration with several
* variants *)
let def = ctx_lookup_type_decl ctx def_id in
- assert (List.length generics.regions = List.length def.generics.regions);
+ cassert (List.length generics.regions = List.length def.generics.regions) meta "T";
(* Retrieve, for every variant, the list of its instantiated field types *)
let variants_fields_types =
AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def
@@ -222,7 +223,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
in
(* Check if there is strictly more than one variant *)
if List.length variants_fields_types > 1 && not expand_enumerations then
- raise (Failure "Not allowed to expand enumerations with several variants");
+ craise meta "Not allowed to expand enumerations with several variants";
(* Initialize the expanded value for a given variant *)
let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
symbolic_expansion =
@@ -260,21 +261,21 @@ let compute_expanded_symbolic_box_value (boxed_ty : rty) : symbolic_expansion =
[expand_enumerations] controls the expansion of enumerations: if [false], it
doesn't allow the expansion of enumerations *containing several variants*.
*)
-let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
+let compute_expanded_symbolic_adt_value (meta : Meta.meta) (expand_enumerations : bool)
(adt_id : type_id) (generics : generic_args) (ctx : eval_ctx) :
symbolic_expansion list =
match (adt_id, generics.regions, generics.types) with
| TAdtId def_id, _, _ ->
- compute_expanded_symbolic_non_assumed_adt_value expand_enumerations def_id
+ compute_expanded_symbolic_non_assumed_adt_value meta expand_enumerations def_id
generics ctx
| TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value generics.types ]
| TAssumed TBox, [], [ boxed_ty ] ->
[ compute_expanded_symbolic_box_value boxed_ty ]
| _ ->
- raise
- (Failure "compute_expanded_symbolic_adt_value: unexpected combination")
+ craise
+ meta "compute_expanded_symbolic_adt_value: unexpected combination"
-let expand_symbolic_value_shared_borrow (config : config)
+let expand_symbolic_value_shared_borrow (meta : Meta.meta) (config : config)
(original_sv : symbolic_value) (original_sv_place : SA.mplace option)
(ref_ty : rty) : cm_fun =
fun cf ctx ->
@@ -307,7 +308,7 @@ let expand_symbolic_value_shared_borrow (config : config)
Some [ AsbBorrow bid; shared_asb ]
else (* Not in the set: ignore *)
Some [ shared_asb ]
- | _ -> raise (Failure "Unexpected")
+ | _ -> craise meta "Unexpected"
else None
in
(* The fresh symbolic value for the shared value *)
@@ -324,7 +325,7 @@ let expand_symbolic_value_shared_borrow (config : config)
else super#visit_VSymbolic env sv
method! visit_EAbs proj_regions abs =
- assert (Option.is_none proj_regions);
+ cassert (Option.is_none proj_regions) meta "T";
let proj_regions = Some abs.regions in
super#visit_EAbs proj_regions abs
@@ -349,7 +350,7 @@ let expand_symbolic_value_shared_borrow (config : config)
method! visit_aproj proj_regions aproj =
(match aproj with
| AProjLoans (sv, _) | AProjBorrows (sv, _) ->
- assert (not (same_symbolic_id sv original_sv))
+ cassert (not (same_symbolic_id sv original_sv)) meta "T"
| AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
super#visit_aproj proj_regions aproj
@@ -375,27 +376,27 @@ let expand_symbolic_value_shared_borrow (config : config)
let ctx = obj#visit_eval_ctx None ctx in
(* Finally, replace the projectors on loans *)
let bids = !borrows in
- assert (not (BorrowId.Set.is_empty bids));
+ cassert (not (BorrowId.Set.is_empty bids)) meta "T";
let see = SeSharedRef (bids, shared_sv) in
let allow_reborrows = true in
let ctx =
- apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
+ apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv see
ctx
in
(* Call the continuation *)
let expr = cf ctx in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place see
+ S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place see
expr
(** TODO: simplify and merge with the other expansion function *)
-let expand_symbolic_value_borrow (config : config)
+let expand_symbolic_value_borrow (meta : Meta.meta) (config : config)
(original_sv : symbolic_value) (original_sv_place : SA.mplace option)
(region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
fun cf ctx ->
- assert (region <> RErased);
+ cassert (region <> RErased) meta "T";
(* Check that we are allowed to expand the reference *)
- assert (not (region_in_set region ctx.ended_regions));
+ cassert (not (region_in_set region ctx.ended_regions)) meta "T";
(* Match on the reference kind *)
match rkind with
| RMut ->
@@ -408,20 +409,20 @@ let expand_symbolic_value_borrow (config : config)
* check that we perform exactly one substitution) *)
let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in
let at_most_once = true in
- let ctx = replace_symbolic_values at_most_once original_sv nv.value ctx in
+ let ctx = replace_symbolic_values meta at_most_once original_sv nv.value ctx in
(* Expand the symbolic avalues *)
let allow_reborrows = true in
let ctx =
- apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+ apply_symbolic_expansion_to_avalues meta config allow_reborrows original_sv
see ctx
in
(* Apply the continuation *)
let expr = cf ctx in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place
+ S.synthesize_symbolic_expansion_no_branching meta original_sv original_sv_place
see expr
| RShared ->
- expand_symbolic_value_shared_borrow config original_sv original_sv_place
+ expand_symbolic_value_shared_borrow meta config original_sv original_sv_place
ref_ty cf ctx
(** A small helper.
@@ -440,12 +441,12 @@ let expand_symbolic_value_borrow (config : config)
We need this continuation separately (i.e., we can't compose it with the
continuations in [see_cf_l]) because we perform a join *before* calling it.
*)
-let apply_branching_symbolic_expansions_non_borrow (config : config)
+let apply_branching_symbolic_expansions_non_borrow (meta : Meta.meta) (config : config)
(sv : symbolic_value) (sv_place : SA.mplace option)
(see_cf_l : (symbolic_expansion option * st_cm_fun) list)
(cf_after_join : st_m_fun) : m_fun =
fun ctx ->
- assert (see_cf_l <> []);
+ cassert (see_cf_l <> []) meta "T";
(* Apply the symbolic expansion in the context and call the continuation *)
let resl =
List.map
@@ -456,7 +457,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
let ctx =
match see_opt with
| None -> ctx
- | Some see -> apply_symbolic_expansion_non_borrow config sv see ctx
+ | Some see -> apply_symbolic_expansion_non_borrow meta config sv see ctx
in
(* Debug *)
log#ldebug
@@ -475,15 +476,15 @@ let apply_branching_symbolic_expansions_non_borrow (config : config)
match resl with
| Some _ :: _ -> Some (List.map Option.get resl)
| None :: _ ->
- List.iter (fun res -> assert (res = None)) resl;
+ List.iter (fun res -> cassert (res = None) meta "T") resl;
None
- | _ -> raise (Failure "Unreachable")
+ | _ -> craise meta "Unreachable"
in
(* Synthesize and return *)
let seel = List.map fst see_cf_l in
- S.synthesize_symbolic_expansion sv sv_place seel subterms
+ S.synthesize_symbolic_expansion meta sv sv_place seel subterms
-let expand_symbolic_bool (config : config) (sv : symbolic_value)
+let expand_symbolic_bool (meta : Meta.meta) (config : config) (sv : symbolic_value)
(sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun)
(cf_after_join : st_m_fun) : m_fun =
fun ctx ->
@@ -491,16 +492,16 @@ let expand_symbolic_bool (config : config) (sv : symbolic_value)
let original_sv = sv in
let original_sv_place = sv_place in
let rty = original_sv.sv_ty in
- assert (rty = TLiteral TBool);
+ cassert (rty = TLiteral TBool) meta "T";
(* Expand the symbolic value to true or false and continue execution *)
let see_true = SeLiteral (VBool true) in
let see_false = SeLiteral (VBool false) in
let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in
(* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
- apply_branching_symbolic_expansions_non_borrow config original_sv
+ apply_branching_symbolic_expansions_non_borrow meta config original_sv
original_sv_place seel cf_after_join ctx
-let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
+let expand_symbolic_value_no_branching (meta : Meta.meta) (config : config) (sv : symbolic_value)
(sv_place : SA.mplace option) : cm_fun =
fun cf ctx ->
(* Debug *)
@@ -522,29 +523,29 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
(* Compute the expanded value *)
let allow_branching = false in
let seel =
- compute_expanded_symbolic_adt_value allow_branching adt_id generics
+ compute_expanded_symbolic_adt_value meta allow_branching adt_id generics
ctx
in
(* There should be exacly one branch *)
let see = Collections.List.to_cons_nil seel in
(* Apply in the context *)
let ctx =
- apply_symbolic_expansion_non_borrow config original_sv see ctx
+ apply_symbolic_expansion_non_borrow meta config original_sv see ctx
in
(* Call the continuation *)
let expr = cf ctx in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion_no_branching original_sv
+ S.synthesize_symbolic_expansion_no_branching meta original_sv
original_sv_place see expr
(* Borrows *)
| TRef (region, ref_ty, rkind) ->
- expand_symbolic_value_borrow config original_sv original_sv_place region
+ expand_symbolic_value_borrow meta config original_sv original_sv_place region
ref_ty rkind cf ctx
| _ ->
- raise
- (Failure
+ craise
+ meta
("expand_symbolic_value_no_branching: unexpected type: "
- ^ show_rty rty))
+ ^ show_rty rty)
in
(* Debug *)
let cc =
@@ -556,12 +557,12 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
(* Sanity check: the symbolic value has disappeared *)
- assert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)))
+ cassert (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta "T")
in
(* Continue *)
cc cf ctx
-let expand_symbolic_adt (config : config) (sv : symbolic_value)
+let expand_symbolic_adt (meta : Meta.meta) (config : config) (sv : symbolic_value)
(sv_place : SA.mplace option) (cf_branches : st_cm_fun)
(cf_after_join : st_m_fun) : m_fun =
fun ctx ->
@@ -579,21 +580,21 @@ let expand_symbolic_adt (config : config) (sv : symbolic_value)
let allow_branching = true in
(* Compute the expanded value *)
let seel =
- compute_expanded_symbolic_adt_value allow_branching adt_id generics ctx
+ compute_expanded_symbolic_adt_value meta allow_branching adt_id generics ctx
in
(* Apply *)
let seel = List.map (fun see -> (Some see, cf_branches)) seel in
- apply_branching_symbolic_expansions_non_borrow config original_sv
+ apply_branching_symbolic_expansions_non_borrow meta config original_sv
original_sv_place seel cf_after_join ctx
| _ ->
- raise (Failure ("expand_symbolic_adt: unexpected type: " ^ show_rty rty))
+ craise meta ("expand_symbolic_adt: unexpected type: " ^ show_rty rty)
-let expand_symbolic_int (config : config) (sv : symbolic_value)
+let expand_symbolic_int (meta : Meta.meta) (config : config) (sv : symbolic_value)
(sv_place : SA.mplace option) (int_type : integer_type)
(tgts : (scalar_value * st_cm_fun) list) (otherwise : st_cm_fun)
(cf_after_join : st_m_fun) : m_fun =
(* Sanity check *)
- assert (sv.sv_ty = TLiteral (TInteger int_type));
+ cassert (sv.sv_ty = TLiteral (TInteger int_type)) meta "T";
(* For all the branches of the switch, we expand the symbolic value
* to the value given by the branch and execute the branch statement.
* For the otherwise branch, we leave the symbolic value as it is
@@ -608,7 +609,7 @@ let expand_symbolic_int (config : config) (sv : symbolic_value)
in
let seel = List.append seel [ (None, otherwise) ] in
(* Then expand and evaluate - this generates the proper symbolic AST *)
- apply_branching_symbolic_expansions_non_borrow config sv sv_place seel
+ apply_branching_symbolic_expansions_non_borrow meta config sv sv_place seel
cf_after_join
(** Expand all the symbolic values which contain borrows.
@@ -619,7 +620,7 @@ let expand_symbolic_int (config : config) (sv : symbolic_value)
an enumeration with strictly more than one variant, a slice, etc.) or if
we need to expand a recursive type (because this leads to looping).
*)
-let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
+let greedy_expand_symbolics_with_borrows (meta : Meta.meta) (config : config) : cm_fun =
fun cf ctx ->
(* The visitor object, to look for symbolic values in the concrete environment *)
let obj =
@@ -660,33 +661,33 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
(match def.kind with
| Struct _ | Enum ([] | [ _ ]) -> ()
| Enum (_ :: _) ->
- raise
- (Failure
+ craise
+ meta
("Attempted to greedily expand a symbolic enumeration \
with > 1 variants (option \
[greedy_expand_symbolics_with_borrows] of [config]): "
- ^ name_to_string ctx def.name))
+ ^ name_to_string ctx def.name)
| Opaque ->
- raise (Failure "Attempted to greedily expand an opaque type"));
+ craise meta "Attempted to greedily expand an opaque type");
(* Also, we need to check if the definition is recursive *)
if ctx_type_decl_is_rec ctx def_id then
- raise
- (Failure
+ craise
+ meta
("Attempted to greedily expand a recursive definition \
(option [greedy_expand_symbolics_with_borrows] of \
[config]): "
- ^ name_to_string ctx def.name))
- else expand_symbolic_value_no_branching config sv None
+ ^ name_to_string ctx def.name)
+ else expand_symbolic_value_no_branching meta config sv None
| TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) ->
(* Ok *)
- expand_symbolic_value_no_branching config sv None
+ expand_symbolic_value_no_branching meta config sv None
| TAdt (TAssumed (TArray | TSlice | TStr), _) ->
(* We can't expand those *)
- raise
- (Failure
- "Attempted to greedily expand an ADT which can't be expanded ")
+ craise
+ meta
+ "Attempted to greedily expand an ADT which can't be expanded "
| TVar _ | TLiteral _ | TNever | TTraitType _ | TArrow _ | TRawPtr _ ->
- raise (Failure "Unreachable")
+ craise meta "Unreachable"
in
(* Compose and continue *)
comp cc expand cf ctx
@@ -694,9 +695,9 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
(* Apply *)
expand cf ctx
-let greedy_expand_symbolic_values (config : config) : cm_fun =
+let greedy_expand_symbolic_values (meta : Meta.meta) (config : config) : cm_fun =
fun cf ctx ->
if Config.greedy_expand_symbolics_with_borrows then (
log#ldebug (lazy "greedy_expand_symbolic_values");
- greedy_expand_symbolics_with_borrows config cf ctx)
+ greedy_expand_symbolics_with_borrows meta config cf ctx)
else cf ctx
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index afbf4605..51be904f 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -23,7 +23,7 @@ let log = Logging.expressions_log
Note that the place should have been prepared so that there are no remaining
loans.
*)
-let expand_primitively_copyable_at_place (config : config)
+let expand_primitively_copyable_at_place (meta : Meta.meta) (config : config)
(access : access_kind) (p : place) : cm_fun =
fun cf ctx ->
(* Small helper *)
@@ -36,7 +36,7 @@ let expand_primitively_copyable_at_place (config : config)
| None -> cf ctx
| Some sv ->
let cc =
- expand_symbolic_value_no_branching config sv (Some (mk_mplace p ctx))
+ expand_symbolic_value_no_branching config sv (Some (mk_mplace meta p ctx))
in
comp cc expand cf ctx
in
@@ -59,7 +59,7 @@ let read_place (access : access_kind) (p : place) (cf : typed_value -> m_fun) :
(* Call the continuation *)
cf v ctx
-let access_rplace_reorganize_and_read (config : config)
+let access_rplace_reorganize_and_read (meta : Meta.meta) (config : config)
(expand_prim_copy : bool) (access : access_kind) (p : place)
(cf : typed_value -> m_fun) : m_fun =
fun ctx ->
@@ -71,7 +71,7 @@ let access_rplace_reorganize_and_read (config : config)
* borrows) *)
let cc =
if expand_prim_copy then
- comp cc (expand_primitively_copyable_at_place config access p)
+ comp cc (expand_primitively_copyable_at_place meta config access p)
else cc
in
(* Read the place - note that this checks that the value doesn't contain bottoms *)
@@ -79,10 +79,10 @@ let access_rplace_reorganize_and_read (config : config)
(* Compose *)
comp cc read_place cf ctx
-let access_rplace_reorganize (config : config) (expand_prim_copy : bool)
+let access_rplace_reorganize (meta : Meta.meta) (config : config) (expand_prim_copy : bool)
(access : access_kind) (p : place) : cm_fun =
fun cf ctx ->
- access_rplace_reorganize_and_read config expand_prim_copy access p
+ access_rplace_reorganize_and_read meta config expand_prim_copy access p
(fun _v -> cf)
ctx
@@ -224,7 +224,7 @@ let rec copy_value (allow_adt_copy : bool) (config : config) (ctx : eval_ctx)
what we do in the formalization (because we don't enforce the same constraints
as MIR in the formalization).
*)
-let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
+let prepare_eval_operand_reorganize (meta : Meta.meta) (config : config) (op : operand) : cm_fun =
fun cf ctx ->
let prepare : cm_fun =
fun cf ctx ->
@@ -237,12 +237,12 @@ let prepare_eval_operand_reorganize (config : config) (op : operand) : cm_fun =
let access = Read in
(* Expand the symbolic values, if necessary *)
let expand_prim_copy = true in
- access_rplace_reorganize config expand_prim_copy access p cf ctx
+ access_rplace_reorganize meta config expand_prim_copy access p cf ctx
| Move p ->
(* Access the value *)
let access = Move in
let expand_prim_copy = false in
- access_rplace_reorganize config expand_prim_copy access p cf ctx
+ access_rplace_reorganize meta config expand_prim_copy access p cf ctx
in
(* Apply *)
prepare cf ctx
@@ -358,7 +358,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
(* Compose and apply *)
comp cc move cf ctx
-let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
+let eval_operand (meta : Meta.meta) (config : config) (op : operand) (cf : typed_value -> m_fun) :
m_fun =
fun ctx ->
(* Debug *)
@@ -368,7 +368,7 @@ let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
^ eval_ctx_to_string ctx ^ "\n"));
(* We reorganize the context, then evaluate the operand *)
comp
- (prepare_eval_operand_reorganize config op)
+ (prepare_eval_operand_reorganize meta config op)
(eval_operand_no_reorganize config op)
cf ctx
@@ -376,16 +376,16 @@ let eval_operand (config : config) (op : operand) (cf : typed_value -> m_fun) :
See [prepare_eval_operand_reorganize].
*)
-let prepare_eval_operands_reorganize (config : config) (ops : operand list) :
+let prepare_eval_operands_reorganize (meta : Meta.meta) (config : config) (ops : operand list) :
cm_fun =
- fold_left_apply_continuation (prepare_eval_operand_reorganize config) ops
+ fold_left_apply_continuation (prepare_eval_operand_reorganize meta config) ops
(** Evaluate several operands. *)
-let eval_operands (config : config) (ops : operand list)
+let eval_operands (meta : Meta.meta) (config : config) (ops : operand list)
(cf : typed_value list -> m_fun) : m_fun =
fun ctx ->
(* Prepare the operands *)
- let prepare = prepare_eval_operands_reorganize config ops in
+ let prepare = prepare_eval_operands_reorganize meta config ops in
(* Evaluate the operands *)
let eval =
fold_left_list_apply_continuation (eval_operand_no_reorganize config) ops
@@ -393,9 +393,9 @@ let eval_operands (config : config) (ops : operand list)
(* Compose and apply *)
comp prepare eval cf ctx
-let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
+let eval_two_operands (meta : Meta.meta) (config : config) (op1 : operand) (op2 : operand)
(cf : typed_value * typed_value -> m_fun) : m_fun =
- let eval_op = eval_operands config [ op1; op2 ] in
+ let eval_op = eval_operands meta config [ op1; op2 ] in
let use_res cf res =
match res with
| [ v1; v2 ] -> cf (v1, v2)
@@ -403,10 +403,10 @@ let eval_two_operands (config : config) (op1 : operand) (op2 : operand)
in
comp eval_op use_res cf
-let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
+let eval_unary_op_concrete (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
(cf : (typed_value, eval_error) result -> m_fun) : m_fun =
(* Evaluate the operand *)
- let eval_op = eval_operand config op in
+ let eval_op = eval_operand meta config op in
(* Apply the unop *)
let apply cf (v : typed_value) : m_fun =
match (unop, v.value) with
@@ -451,11 +451,11 @@ let eval_unary_op_concrete (config : config) (unop : unop) (op : operand)
in
comp eval_op apply cf
-let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
+let eval_unary_op_symbolic (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
(cf : (typed_value, eval_error) result -> m_fun) : m_fun =
fun ctx ->
(* Evaluate the operand *)
- let eval_op = eval_operand config op in
+ let eval_op = eval_operand meta config op in
(* Generate a fresh symbolic value to store the result *)
let apply cf (v : typed_value) : m_fun =
fun ctx ->
@@ -472,17 +472,17 @@ let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
(* Synthesize the symbolic AST *)
synthesize_unary_op ctx unop v
- (mk_opt_place_from_op op ctx)
+ (mk_opt_place_from_op meta op ctx)
res_sv None expr
in
(* Compose and apply *)
comp eval_op apply cf ctx
-let eval_unary_op (config : config) (unop : unop) (op : operand)
+let eval_unary_op (meta : Meta.meta) (config : config) (unop : unop) (op : operand)
(cf : (typed_value, eval_error) result -> m_fun) : m_fun =
match config.mode with
- | ConcreteMode -> eval_unary_op_concrete config unop op cf
- | SymbolicMode -> eval_unary_op_symbolic config unop op cf
+ | ConcreteMode -> eval_unary_op_concrete meta config unop op cf
+ | SymbolicMode -> eval_unary_op_symbolic meta config unop op cf
(** Small helper for [eval_binary_op_concrete]: computes the result of applying
the binop *after* the operands have been successfully evaluated
@@ -557,10 +557,10 @@ let eval_binary_op_concrete_compute (binop : binop) (v1 : typed_value)
| Ne | Eq -> raise (Failure "Unreachable"))
| _ -> raise (Failure "Invalid inputs for binop")
-let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_concrete (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
(op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
(* Evaluate the operands *)
- let eval_ops = eval_two_operands config op1 op2 in
+ let eval_ops = eval_two_operands meta config op1 op2 in
(* Compute the result of the binop *)
let compute cf (res : typed_value * typed_value) =
let v1, v2 = res in
@@ -569,11 +569,11 @@ let eval_binary_op_concrete (config : config) (binop : binop) (op1 : operand)
(* Compose and apply *)
comp eval_ops compute cf
-let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op_symbolic (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
(op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
fun ctx ->
(* Evaluate the operands *)
- let eval_ops = eval_two_operands config op1 op2 in
+ let eval_ops = eval_two_operands meta config op1 op2 in
(* Compute the result of applying the binop *)
let compute cf ((v1, v2) : typed_value * typed_value) : m_fun =
fun ctx ->
@@ -609,20 +609,20 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
let v = mk_typed_value_from_symbolic_value res_sv in
let expr = cf (Ok v) ctx in
(* Synthesize the symbolic AST *)
- let p1 = mk_opt_place_from_op op1 ctx in
- let p2 = mk_opt_place_from_op op2 ctx in
+ let p1 = mk_opt_place_from_op meta op1 ctx in
+ let p2 = mk_opt_place_from_op meta op2 ctx in
synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr
in
(* Compose and apply *)
comp eval_ops compute cf ctx
-let eval_binary_op (config : config) (binop : binop) (op1 : operand)
+let eval_binary_op (meta : Meta.meta) (config : config) (binop : binop) (op1 : operand)
(op2 : operand) (cf : (typed_value, eval_error) result -> m_fun) : m_fun =
match config.mode with
- | ConcreteMode -> eval_binary_op_concrete config binop op1 op2 cf
- | SymbolicMode -> eval_binary_op_symbolic config binop op1 op2 cf
+ | ConcreteMode -> eval_binary_op_concrete meta config binop op1 op2 cf
+ | SymbolicMode -> eval_binary_op_symbolic meta config binop op1 op2 cf
-let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
+let eval_rvalue_ref (meta : Meta.meta) (config : config) (p : place) (bkind : borrow_kind)
(cf : typed_value -> m_fun) : m_fun =
fun ctx ->
match bkind with
@@ -643,7 +643,7 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
let expand_prim_copy = false in
let prepare =
- access_rplace_reorganize_and_read config expand_prim_copy access p
+ access_rplace_reorganize_and_read meta config expand_prim_copy access p
in
(* Evaluate the borrowing operation *)
let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -693,7 +693,7 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
let access = Write in
let expand_prim_copy = false in
let prepare =
- access_rplace_reorganize_and_read config expand_prim_copy access p
+ access_rplace_reorganize_and_read meta config expand_prim_copy access p
in
(* Evaluate the borrowing operation *)
let eval (cf : typed_value -> m_fun) (v : typed_value) : m_fun =
@@ -714,10 +714,10 @@ let eval_rvalue_ref (config : config) (p : place) (bkind : borrow_kind)
(* Compose and apply *)
comp prepare eval cf ctx
-let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
+let eval_rvalue_aggregate (meta : Meta.meta) (config : config) (aggregate_kind : aggregate_kind)
(ops : operand list) (cf : typed_value -> m_fun) : m_fun =
(* Evaluate the operands *)
- let eval_ops = eval_operands config ops in
+ let eval_ops = eval_operands meta config ops in
(* Compute the value *)
let compute (cf : typed_value -> m_fun) (values : typed_value list) : m_fun =
fun ctx ->
@@ -781,7 +781,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
(* Compose and apply *)
comp eval_ops compute cf
-let eval_rvalue_not_global (config : config) (rvalue : rvalue)
+let eval_rvalue_not_global (meta : Meta.meta) (config : config) (rvalue : rvalue)
(cf : (typed_value, eval_error) result -> m_fun) : m_fun =
fun ctx ->
log#ldebug (lazy "eval_rvalue");
@@ -793,12 +793,12 @@ let eval_rvalue_not_global (config : config) (rvalue : rvalue)
let comp_wrap f = comp f wrap_in_result cf in
(* Delegate to the proper auxiliary function *)
match rvalue with
- | Use op -> comp_wrap (eval_operand config op) ctx
- | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref config p bkind) ctx
- | UnaryOp (unop, op) -> eval_unary_op config unop op cf ctx
- | BinaryOp (binop, op1, op2) -> eval_binary_op config binop op1 op2 cf ctx
+ | Use op -> comp_wrap (eval_operand meta config op) ctx
+ | RvRef (p, bkind) -> comp_wrap (eval_rvalue_ref meta config p bkind) ctx
+ | UnaryOp (unop, op) -> eval_unary_op meta config unop op cf ctx
+ | BinaryOp (binop, op1, op2) -> eval_binary_op meta config binop op1 op2 cf ctx
| Aggregate (aggregate_kind, ops) ->
- comp_wrap (eval_rvalue_aggregate config aggregate_kind ops) ctx
+ comp_wrap (eval_rvalue_aggregate meta config aggregate_kind ops) ctx
| Discriminant _ ->
raise
(Failure
@@ -806,11 +806,11 @@ let eval_rvalue_not_global (config : config) (rvalue : rvalue)
the AST")
| Global _ -> raise (Failure "Unreachable")
-let eval_fake_read (config : config) (p : place) : cm_fun =
+let eval_fake_read (meta : Meta.meta) (config : config) (p : place) : cm_fun =
fun cf ctx ->
let expand_prim_copy = false in
let cf_prepare cf =
- access_rplace_reorganize_and_read config expand_prim_copy Read p cf
+ access_rplace_reorganize_and_read meta config expand_prim_copy Read p cf
in
let cf_continue cf v : m_fun =
fun ctx ->
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index b07ba943..35582456 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -693,7 +693,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
AbstractionId.of_int (RegionGroupId.to_int rg_id)
in
(* By default, the [SynthInput] abs can't end *)
- let ctx = ctx_set_abs_can_end ctx abs_id true in
+ let ctx = ctx_set_abs_can_end meta ctx abs_id true in
cassert (
let abs = ctx_lookup_abs ctx abs_id in
abs.kind = SynthInput rg_id) meta "TODO : error message ";
@@ -764,7 +764,7 @@ let compute_loop_entry_fixed_point (meta : Meta.meta) (config : config) (loop_id
in
let abs = ctx_lookup_abs !fp !id0 in
let abs = { abs with kind = abs_kind } in
- let fp', _ = ctx_subst_abs !fp !id0 abs in
+ let fp', _ = ctx_subst_abs meta !fp !id0 abs in
fp := fp';
(* Merge all the abstractions into this one *)
List.iter
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index e411db9b..cc1e3208 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -259,13 +259,13 @@ let access_place (meta : Meta.meta) (access : projection_access)
(update : typed_value -> typed_value) (p : place) (ctx : eval_ctx) :
(eval_ctx * typed_value) path_access_result =
(* Lookup the variable's value *)
- let value = ctx_lookup_var_value ctx p.var_id in
+ let value = ctx_lookup_var_value meta ctx p.var_id in
(* Apply the projection *)
match access_projection meta access ctx update p.projection value with
| Error err -> Error err
| Ok (ctx, res) ->
(* Update the value *)
- let ctx = ctx_update_var_value ctx p.var_id res.updated in
+ let ctx = ctx_update_var_value meta ctx p.var_id res.updated in
(* Return *)
Ok (ctx, res.read)
@@ -465,7 +465,7 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
in
let prefix = { p with projection = proj } in
expand_symbolic_value_no_branching config sp
- (Some (Synth.mk_mplace prefix ctx))
+ (Some (Synth.mk_mplace meta prefix ctx))
| FailBottom (_, _, _) ->
(* We can't expand {!Bottom} values while reading them *)
craise meta "Found [Bottom] while reading a place"
@@ -490,7 +490,7 @@ let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (acces
| FailSymbolic (_pe, sp) ->
(* Expand the symbolic value *)
expand_symbolic_value_no_branching config sp
- (Some (Synth.mk_mplace p ctx))
+ (Some (Synth.mk_mplace meta p ctx))
| FailBottom (remaining_pes, pe, ty) ->
(* Expand the {!Bottom} value *)
fun cf ctx ->
@@ -575,7 +575,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
let rec drop : cm_fun =
fun cf ctx ->
(* Read the value *)
- let v = ctx_lookup_dummy_var ctx dummy_id in
+ let v = ctx_lookup_dummy_var meta ctx dummy_id in
(* Check if there are loans or borrows to end *)
let with_borrows = false in
match get_first_outer_loan_or_borrow_in_value with_borrows v with
@@ -599,7 +599,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
let cc =
comp cc (fun cf ctx ->
(* Pop *)
- let ctx, v = ctx_remove_dummy_var ctx dummy_id in
+ let ctx, v = ctx_remove_dummy_var meta ctx dummy_id in
(* Reinsert *)
let ctx = write_place meta access p v ctx in
(* Sanity check *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index bd6fab1a..8ccdcc93 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -58,33 +58,33 @@ let push_dummy_var (vid : DummyVarId.id) (v : typed_value) : cm_fun =
cf ctx
(** Remove a dummy variable from the environment *)
-let remove_dummy_var (vid : DummyVarId.id) (cf : typed_value -> m_fun) : m_fun =
+let remove_dummy_var (meta : Meta.meta) (vid : DummyVarId.id) (cf : typed_value -> m_fun) : m_fun =
fun ctx ->
- let ctx, v = ctx_remove_dummy_var ctx vid in
+ let ctx, v = ctx_remove_dummy_var meta ctx vid in
cf v ctx
(** Push an uninitialized variable to the environment *)
-let push_uninitialized_var (var : var) : cm_fun =
+let push_uninitialized_var (meta : Meta.meta) (var : var) : cm_fun =
fun cf ctx ->
- let ctx = ctx_push_uninitialized_var ctx var in
+ let ctx = ctx_push_uninitialized_var meta ctx var in
cf ctx
(** Push a list of uninitialized variables to the environment *)
-let push_uninitialized_vars (vars : var list) : cm_fun =
+let push_uninitialized_vars (meta : Meta.meta) (vars : var list) : cm_fun =
fun cf ctx ->
- let ctx = ctx_push_uninitialized_vars ctx vars in
+ let ctx = ctx_push_uninitialized_vars meta ctx vars in
cf ctx
(** Push a variable to the environment *)
-let push_var (var : var) (v : typed_value) : cm_fun =
+let push_var (meta : Meta.meta) (var : var) (v : typed_value) : cm_fun =
fun cf ctx ->
- let ctx = ctx_push_var ctx var v in
+ let ctx = ctx_push_var meta ctx var v in
cf ctx
(** Push a list of variables to the environment *)
-let push_vars (vars : (var * typed_value) list) : cm_fun =
+let push_vars (meta : Meta.meta) (vars : (var * typed_value) list) : cm_fun =
fun cf ctx ->
- let ctx = ctx_push_vars ctx vars in
+ let ctx = ctx_push_vars meta ctx vars in
cf ctx
(** Assign a value to a given place.
@@ -108,7 +108,7 @@ let assign_to_place (meta : Meta.meta) (config : config) (rv : typed_value) (p :
(* Prepare the destination *)
let cc = comp cc (prepare_lplace config p) in
(* Retrieve the rvalue from the dummy variable *)
- let cc = comp cc (fun cf _lv -> remove_dummy_var rvalue_vid cf) in
+ let cc = comp cc (fun cf _lv -> remove_dummy_var meta rvalue_vid cf) in
(* Update the destination *)
let move_dest cf (rv : typed_value) : m_fun =
fun ctx ->
@@ -538,7 +538,7 @@ let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fi
let ret_vid = VarId.zero in
let ret_ty = get_assumed_function_return_type meta ctx fid generics in
let ret_var = mk_var ret_vid (Some "@return") ret_ty in
- let cc = comp cc (push_uninitialized_var ret_var) in
+ let cc = comp cc (push_uninitialized_var meta ret_var) in
(* Create and push the input variables *)
let input_vars =
@@ -546,7 +546,7 @@ let eval_assumed_function_call_concrete (meta : Meta.meta) (config : config) (fi
(fun id (v : typed_value) -> (mk_var id None v.ty, v))
args_vl
in
- let cc = comp cc (push_vars input_vars) in
+ let cc = comp cc (push_vars meta input_vars) in
(* "Execute" the function body. As the functions are assumed, here we call
* custom functions to perform the proper manipulations: we don't have
@@ -981,10 +981,10 @@ let rec eval_statement (meta : Meta.meta) (config : config) (st : statement) : s
let rp = rvalue_get_place rvalue in
let rp =
match rp with
- | Some rp -> Some (S.mk_mplace rp ctx)
+ | Some rp -> Some (S.mk_mplace meta rp ctx)
| None -> None
in
- S.synthesize_assignment ctx (S.mk_mplace p ctx) rv rp expr
+ S.synthesize_assignment ctx (S.mk_mplace meta p ctx) rv rp expr
)
in
@@ -1094,7 +1094,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
let cf_true : st_cm_fun = eval_statement meta config st1 in
let cf_false : st_cm_fun = eval_statement meta config st2 in
expand_symbolic_bool config sv
- (S.mk_opt_place_from_op op ctx)
+ (S.mk_opt_place_from_op meta op ctx)
cf_true cf_false cf ctx
| _ -> craise meta "Inconsistent state"
in
@@ -1141,7 +1141,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
let otherwise = eval_statement meta config otherwise in
(* Expand and continue *)
expand_symbolic_int config sv
- (S.mk_opt_place_from_op op ctx)
+ (S.mk_opt_place_from_op meta op ctx)
int_ty stgts otherwise cf ctx
| _ -> craise meta "Inconsistent state"
in
@@ -1175,7 +1175,7 @@ and eval_switch (meta : Meta.meta) (config : config) (switch : switch) : st_cm_f
| VSymbolic sv ->
(* Expand the symbolic value - may lead to branching *)
let cf_expand =
- expand_symbolic_adt config sv (Some (S.mk_mplace p ctx))
+ expand_symbolic_adt config sv (Some (S.mk_mplace meta p ctx))
in
(* Re-evaluate the switch - the value is not symbolic anymore,
which means we will go to the other branch *)
@@ -1280,7 +1280,7 @@ and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
in
let cc =
- comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty))
+ comp_transmit cc (push_var meta ret_var (mk_bottom ret_var.var_ty))
in
(* 2. Push the input values *)
@@ -1288,12 +1288,12 @@ and eval_transparent_function_call_concrete (meta : Meta.meta) (config : config)
let inputs = List.combine input_locals args in
(* Note that this function checks that the variables and their values
* have the same type (this is important) *)
- push_vars inputs cf
+ push_vars meta inputs cf
in
let cc = comp cc cf_push_inputs in
(* 3. Push the remaining local variables (initialized as {!Bottom}) *)
- let cc = comp cc (push_uninitialized_vars locals) in
+ let cc = comp cc (push_uninitialized_vars meta locals) in
(* Execute the function body *)
let cc = comp cc (eval_function_body meta config body_st) in
@@ -1366,8 +1366,8 @@ and eval_function_call_symbolic_from_inst_sig (meta : Meta.meta) (config : confi
let ret_av regions =
mk_aproj_loans_value_from_symbolic_value regions ret_spc
in
- let args_places = List.map (fun p -> S.mk_opt_place_from_op p ctx) args in
- let dest_place = Some (S.mk_mplace dest ctx) in
+ let args_places = List.map (fun p -> S.mk_opt_place_from_op meta p ctx) args in
+ let dest_place = Some (S.mk_mplace meta dest ctx) in
(* Evaluate the input operands *)
let cc = eval_operands config args in
diff --git a/compiler/Main.ml b/compiler/Main.ml
index e4e4ce1f..bea7e4a8 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -271,7 +271,7 @@ let () =
(* Some options for the execution *)
(* Test the unit functions with the concrete interpreter *)
- if !test_unit_functions then Test.test_unit_functions m;
+ if !test_unit_functions then Test.test_unit_functions meta m;
(* Translate the functions *)
Aeneas.Translate.translate_crate meta filename dest_dir m;
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index ad34c48e..787bfb4f 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -4,21 +4,22 @@ open Expressions
open Values
open LlbcAst
open SymbolicAst
+open Errors
-let mk_mplace (p : place) (ctx : Contexts.eval_ctx) : mplace =
- let bv = Contexts.ctx_lookup_var_binder ctx p.var_id in
+let mk_mplace (meta : Meta.meta) (p : place) (ctx : Contexts.eval_ctx) : mplace =
+ let bv = Contexts.ctx_lookup_var_binder meta ctx p.var_id in
{ bv; projection = p.projection }
-let mk_opt_mplace (p : place option) (ctx : Contexts.eval_ctx) : mplace option =
- Option.map (fun p -> mk_mplace p ctx) p
+let mk_opt_mplace (meta : Meta.meta) (p : place option) (ctx : Contexts.eval_ctx) : mplace option =
+ Option.map (fun p -> mk_mplace meta p ctx) p
-let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) :
+let mk_opt_place_from_op (meta : Meta.meta) (op : operand) (ctx : Contexts.eval_ctx) :
mplace option =
- match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None
+ match op with Copy p | Move p -> Some (mk_mplace meta p ctx) | Constant _ -> None
let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e)
-let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
+let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (place : mplace option)
(seel : symbolic_expansion option list) (el : expression list option) :
expression option =
match el with
@@ -36,7 +37,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
(Some (SeLiteral (VBool false)), false_exp);
] ->
ExpandBool (true_exp, false_exp)
- | _ -> raise (Failure "Ill-formed boolean expansion"))
+ | _ -> craise meta "Ill-formed boolean expansion")
| TLiteral (TInteger int_ty) ->
(* Switch over an integer: split between the "regular" branches
and the "otherwise" branch (which should be the last branch) *)
@@ -46,9 +47,9 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
let get_scalar (see : symbolic_expansion option) : scalar_value =
match see with
| Some (SeLiteral (VScalar cv)) ->
- assert (cv.int_ty = int_ty);
+ cassert (cv.int_ty = int_ty) meta "For all the regular branches, the symbolic value should have been expanded to a constant TODO: Error message";
cv
- | _ -> raise (Failure "Unreachable")
+ | _ -> craise meta "Unreachable"
in
let branches =
List.map (fun (see, exp) -> (get_scalar see, exp)) branches
@@ -56,7 +57,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
(* For the otherwise branch, the symbolic value should have been left
* unchanged *)
let otherwise_see, otherwise = otherwise in
- assert (otherwise_see = None);
+ cassert (otherwise_see = None) meta "For the otherwise branch, the symbolic value should have been left unchanged";
(* Return *)
ExpandInt (int_ty, branches, otherwise)
| TAdt (_, _) ->
@@ -65,7 +66,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
VariantId.id option * symbolic_value list =
match see with
| Some (SeAdt (vid, fields)) -> (vid, fields)
- | _ -> raise (Failure "Ill-formed branching ADT expansion")
+ | _ -> craise meta "Ill-formed branching ADT expansion"
in
let exp =
List.map
@@ -79,18 +80,18 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
(* Reference expansion: there should be one branch *)
match ls with
| [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
- | _ -> raise (Failure "Ill-formed borrow expansion"))
+ | _ -> craise meta "Ill-formed borrow expansion")
| TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _
->
- raise (Failure "Ill-formed symbolic expansion")
+ craise meta "Ill-formed symbolic expansion"
in
Some (Expansion (place, sv, expansion))
-let synthesize_symbolic_expansion_no_branching (sv : symbolic_value)
+let synthesize_symbolic_expansion_no_branching (meta : Meta.meta) (sv : symbolic_value)
(place : mplace option) (see : symbolic_expansion) (e : expression option) :
expression option =
let el = Option.map (fun e -> [ e ]) e in
- synthesize_symbolic_expansion sv place [ Some see ] el
+ synthesize_symbolic_expansion meta sv place [ Some see ] el
let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
(sg : fun_sig option) (regions_hierarchy : region_var_groups)
@@ -188,7 +189,7 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
loop_expr;
meta;
})
- | _ -> raise (Failure "Unreachable")
+ | _ -> craise meta "Unreachable"
let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) :
expression option =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 04aadafe..43d2fbb0 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -20,7 +20,7 @@ type symbolic_fun_translation = symbolic_value list * SA.expression
(** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
for the forward function and the backward functions.
*)
-let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
+let translate_function_to_symbolics (meta : Meta.meta) (trans_ctx : trans_ctx) (fdef : fun_decl) :
symbolic_fun_translation option =
(* Debug *)
log#ldebug
@@ -32,7 +32,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
| Some _ ->
(* Evaluate *)
let synthesize = true in
- let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
+ let inputs, symb = evaluate_function_symbolic meta synthesize trans_ctx fdef in
Some (inputs, Option.get symb)
(** Translate a function, by generating its forward and backward translations.
@@ -50,7 +50,7 @@ let translate_function_to_pure (meta : Meta.meta) (trans_ctx : trans_ctx)
(lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.name));
(* Compute the symbolic ASTs, if the function is transparent *)
- let symbolic_trans = translate_function_to_symbolics trans_ctx fdef in
+ let symbolic_trans = translate_function_to_symbolics meta trans_ctx fdef in
(* Convert the symbolic ASTs to pure ASTs: *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 05:31:30 +0000