Merge pull request #151 from AeneasVerif/son/fix-loops2

Fix an issue in the loops fixed point

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