summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/FunsAnalysis.ml3
-rw-r--r--compiler/Interpreter.ml31
-rw-r--r--compiler/InterpreterStatements.ml10
-rw-r--r--compiler/RegionsHierarchy.ml3
-rw-r--r--compiler/SymbolicToPure.ml24
5 files changed, 47 insertions, 24 deletions
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index d98efc8d..ddfbf312 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -147,7 +147,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
(* Sanity check: global bodies don't contain stateful calls *)
cassert __FILE__ __LINE__
((not f.is_global_decl_body) || not !stateful)
- f.item_meta.meta "Global definition containing a stateful call in its body";
+ f.item_meta.meta
+ "Global definition containing a stateful call in its body";
let builtin_info = get_builtin_info f in
let has_builtin_info = builtin_info <> None in
group_has_builtin_info := !group_has_builtin_info || has_builtin_info;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index d9af063e..f10c8d3e 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -218,12 +218,14 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
at the same time the normalization map for the associated types.
*)
let ctx, inst_sg =
- symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature regions_hierarchy
- fdef.kind
+ symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature
+ regions_hierarchy fdef.kind
in
(* Create fresh symbolic values for the inputs *)
let input_svs =
- List.map (fun ty -> mk_fresh_symbolic_value fdef.item_meta.meta ty) inst_sg.inputs
+ List.map
+ (fun ty -> mk_fresh_symbolic_value fdef.item_meta.meta ty)
+ inst_sg.inputs
in
(* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
let call_id = fresh_fun_call_id () in
@@ -299,8 +301,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
in
let _, ret_inst_sg =
- symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature regions_hierarchy
- fdef.kind
+ symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature
+ regions_hierarchy fdef.kind
in
let ret_rty = ret_inst_sg.output in
(* Move the return value out of the return variable *)
@@ -333,8 +335,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
eval_ctx * typed_avalue list =
let ctx, avalue =
- apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx abs.regions
- abs.ancestors_regions ret_value ret_rty
+ apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx
+ abs.regions abs.ancestors_regions ret_value ret_rty
in
(ctx, [ avalue ])
in
@@ -349,7 +351,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
let region_can_end rid =
RegionGroupId.Set.mem rid parent_and_current_rgs
in
- sanity_check __FILE__ __LINE__ (region_can_end back_id) fdef.item_meta.meta;
+ sanity_check __FILE__ __LINE__ (region_can_end back_id)
+ fdef.item_meta.meta;
let ctx =
create_push_abstractions_from_abs_region_groups
(fun rg_id -> SynthRet rg_id)
@@ -534,7 +537,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
let fwd_e =
(* Pop the frame and retrieve the returned value at the same time*)
let pop_return_value = true in
- let cf_pop = pop_frame config fdef.item_meta.meta pop_return_value in
+ let cf_pop =
+ pop_frame config fdef.item_meta.meta pop_return_value
+ in
(* Generate the Return node *)
let cf_return ret_value : m_fun =
fun ctx -> Some (SA.Return (ctx, ret_value))
@@ -584,7 +589,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
(* Pop the frame - there is no returned value to pop: in the
translation we will simply call the loop function *)
let pop_return_value = false in
- let cf_pop = pop_frame config fdef.item_meta.meta pop_return_value in
+ let cf_pop =
+ pop_frame config fdef.item_meta.meta pop_return_value
+ in
(* Generate the Return node *)
let cf_return _ret_value : m_fun =
fun _ctx -> Some (SA.ReturnWithLoop (loop_id, inside_loop))
@@ -668,7 +675,9 @@ module Test = struct
| Return ->
(* Ok: drop the local variables and finish *)
let pop_return_value = true in
- pop_frame config fdef.item_meta.meta pop_return_value (fun _ _ -> None) ctx
+ pop_frame config fdef.item_meta.meta pop_return_value
+ (fun _ _ -> None)
+ ctx
| _ ->
craise __FILE__ __LINE__ fdef.item_meta.meta
("Unit test failed (concrete execution) on: "
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 064fff29..9ad6487b 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1063,8 +1063,8 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
(* Treat the evaluation of the global as a call to the global body *)
let func = { func = FunId (FRegular global.body); generics } in
let call = { func = FnOpRegular func; args = []; dest } in
- (eval_transparent_function_call_concrete config global.item_meta.meta global.body
- call)
+ (eval_transparent_function_call_concrete config global.item_meta.meta
+ global.body call)
cf ctx
| SymbolicMode ->
(* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
@@ -1381,9 +1381,9 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
(inst_sg.output :: inst_sg.inputs))
meta "ADTs containing borrows are not supported yet";
(* Evaluate the function call *)
- eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func def.signature
- regions_hierarchy inst_sg generics trait_method_generics call.args call.dest
- cf ctx
+ eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func
+ def.signature regions_hierarchy inst_sg generics trait_method_generics
+ call.args call.dest cf ctx
(** Evaluate a function call in symbolic mode by using the function signature.
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index c05e9f24..21be89ee 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -323,7 +323,8 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t)
List.map
(fun ((fid, d) : FunDeclId.id * fun_decl) ->
( FRegular fid,
- (Types.name_to_string env d.name, d.signature, Some d.item_meta.meta) ))
+ (Types.name_to_string env d.name, d.signature, Some d.item_meta.meta)
+ ))
(FunDeclId.Map.bindings fun_decls)
in
let assumed =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2fa68329..46135f09 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1262,7 +1262,9 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
let regions_hierarchy =
FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies
in
- let meta = (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).item_meta.meta in
+ let meta =
+ (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).item_meta.meta
+ in
translate_fun_sig_with_regions_hierarchy_to_decomposed meta decls_ctx
(FunId (FRegular fun_id)) regions_hierarchy sg input_names
@@ -3955,10 +3957,14 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
(Print.Contexts.decls_ctx_to_fmt_env ctx)
llbc_name
in
- let generics = translate_generic_params trait_decl.item_meta.meta llbc_generics in
+ let generics =
+ translate_generic_params trait_decl.item_meta.meta llbc_generics
+ in
let preds = translate_predicates trait_decl.item_meta.meta preds in
let parent_clauses =
- List.map (translate_trait_clause trait_decl.item_meta.meta) llbc_parent_clauses
+ List.map
+ (translate_trait_clause trait_decl.item_meta.meta)
+ llbc_parent_clauses
in
let consts =
List.map
@@ -3970,8 +3976,12 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
List.map
(fun (name, (trait_clauses, ty)) ->
( name,
- ( List.map (translate_trait_clause trait_decl.item_meta.meta) trait_clauses,
- Option.map (translate_fwd_ty trait_decl.item_meta.meta type_infos) ty ) ))
+ ( List.map
+ (translate_trait_clause trait_decl.item_meta.meta)
+ trait_clauses,
+ Option.map
+ (translate_fwd_ty trait_decl.item_meta.meta type_infos)
+ ty ) ))
types
in
{
@@ -4020,7 +4030,9 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
(Print.Contexts.decls_ctx_to_fmt_env ctx)
llbc_name
in
- let generics = translate_generic_params trait_impl.item_meta.meta llbc_generics in
+ let generics =
+ translate_generic_params trait_impl.item_meta.meta llbc_generics
+ in
let preds = translate_predicates trait_impl.item_meta.meta preds in
let parent_trait_refs =
List.map (translate_strait_ref trait_impl.item_meta.meta) parent_trait_refs