diff options
| -rw-r--r-- | compiler/FunsAnalysis.ml | 3 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 31 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 40 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 10 | ||||
| -rw-r--r-- | compiler/RegionsHierarchy.ml | 3 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 28 |
6 files changed, 80 insertions, 35 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/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index e710ed2b..3db68f5d 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -714,7 +714,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct both borrows *) raise (ValueMatchFailure (LoanInLeft id0)) - let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx) + let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx) (sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value = let id0 = sv0.sv_id in let id1 = sv1.sv_id in @@ -729,11 +729,18 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct sanity_check __FILE__ __LINE__ (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta; - (* We simply introduce a fresh symbolic value *) + (* TODO: the symbolic values may contain bottoms: we're being conservatice, + and fail (for now) if part of a symbolic value contains a bottom. + A more general approach would be to introduce a symbolic value + with some ended regions. *) + sanity_check __FILE__ __LINE__ + ((not (symbolic_value_has_ended_regions ctx0.ended_regions sv0)) + && not (symbolic_value_has_ended_regions ctx1.ended_regions sv1)) + meta; mk_fresh_symbolic_value meta sv0.sv_ty) - let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool) - (sv : symbolic_value) (v : typed_value) : typed_value = + let match_symbolic_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) + (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = (* Check that: - there are no borrows in the symbolic value - there are no borrows in the "regular" value @@ -763,8 +770,16 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct | Some (VMutLoan id) -> if value_is_left then raise (ValueMatchFailure (LoanInLeft id)) else raise (ValueMatchFailure (LoanInRight id))); - (* Return a fresh symbolic value *) - mk_fresh_symbolic_typed_value meta sv.sv_ty + + (* There might be a bottom in the other value. We're being conservative: + if there is a bottom anywhere (it includes the case where part of the + value contains bottom) the result of the join is bottom. Otherwise, + we generate a fresh symbolic value. *) + if + symbolic_value_has_ended_regions ctx0.ended_regions sv + || bottom_in_value ctx1.ended_regions v + then mk_bottom meta sv.sv_ty + else mk_fresh_symbolic_typed_value meta sv.sv_ty let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool) (v : typed_value) : typed_value = @@ -903,9 +918,16 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct (sv1 : symbolic_value) : symbolic_value = sv1 - let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) - (sv : symbolic_value) (v : typed_value) : typed_value = - if left then v else mk_typed_value_from_symbolic_value sv + let match_symbolic_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) + (left : bool) (sv : symbolic_value) (v : typed_value) : typed_value = + (* We're being conservative for now: if any of the two values contains + a bottom, the join is bottom *) + if + symbolic_value_has_ended_regions ctx0.ended_regions sv + || bottom_in_value ctx1.ended_regions v + then mk_bottom meta sv.sv_ty + else if left then v + else mk_typed_value_from_symbolic_value sv let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool) (v : typed_value) : typed_value = 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..6c925bcd 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -618,7 +618,7 @@ let translate_type_id (meta : Meta.meta) (id : T.type_id) : type_id = | T.TBox -> (* Boxes have to be eliminated: this type id shouldn't be translated *) - craise __FILE__ __LINE__ meta "Unreachable" + craise __FILE__ __LINE__ meta "Unexpected box type" in TAssumed aty | TTuple -> TTuple @@ -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 @@ -1624,7 +1626,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx) let cons = { e = cons_e; ty = cons_ty } in (* Apply the constructor *) mk_apps ctx.meta cons field_values) - | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unreachable" + | VBottom -> craise __FILE__ __LINE__ ctx.meta "Unexpected bottom value" | VLoan lc -> ( match lc with | VSharedLoan (_, v) -> translate v @@ -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 |