Fix a bug in the pre-pass which eliminates loop breaks

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-2193aa00fd89e991226ada10d8a8f66e0594f212
+5d2b6ceba0f5fb83f700baeea8d31df4027d06bf

compiler/InterpreterLoops.ml

@@ -395,7 +395,7 @@ let eval_loop (config : config) (span : span) (eval_loop_body : stl_cm_fun) :
       in
 
       (* We want to make sure the loop will *not* manipulate shared avalues
-         containing themselves shared loans (i.e., nested shared loans in
+         themselves containing shared loans (i.e., nested shared loans in
          the abstractions), because it complexifies the matches between values
          (when joining environments, or checking that two environments are
          equivalent).

compiler/InterpreterLoopsMatchCtxs.ml

@@ -1410,9 +1410,13 @@ let match_ctxs (span : Meta.span) (check_equiv : bool) (fixed_ids : ids_sets)
 
     log#ldebug (lazy "match_abstractions: matching values");
     let _ =
-      List.map
-        (fun (v0, v1) -> M.match_typed_avalues ctx0 ctx1 v0 v1)
-        (List.combine avalues0 avalues1)
+      if List.length avalues0 <> List.length avalues1 then
+        raise
+          (Distinct "Region abstractions with not the same number of values")
+      else
+        List.map
+          (fun (v0, v1) -> M.match_typed_avalues ctx0 ctx1 v0 v1)
+          (List.combine avalues0 avalues1)
     in
     log#ldebug (lazy "match_abstractions: values matched OK");
     ()

compiler/PrePasses.ml

@@ -191,7 +191,33 @@ let remove_useless_cf_merges (crate : crate) (f : fun_decl) : fun_decl =
         }
       };
     ]}
- *)
+
+    We also insert the statements occurring after branchings (matches or
+    if then else) inside the branches. For instance:
+    {[
+      if b {
+        s0;
+      }
+      else {
+        s1;
+      }
+      return;
+
+        ~~>
+
+      if b {
+        s0;
+        return;
+      }
+      else {
+        s1;
+        return;
+      }
+    ]}
+
+    This is necessary because loops might appear inside branchings: if we don't
+    do this some paths inside the loop might not end with a break/continue/return.Aeneas
+  *)
 let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
   let f0 = f in
 
@@ -229,35 +255,48 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
           | Break i ->
               cassert __FILE__ __LINE__ (i = 0) st.span
                 "Breaks to outer loops are not supported yet";
-              { st with content = nst.content }
+              {
+                st with
+                content = nst.content;
+                comments_before = st.comments_before @ nst.comments_before;
+              }
           | _ -> super#visit_statement entered_loop st
       end
     in
     obj#visit_statement false st
   in
 
   (* The visitor *)
-  let obj =
+  let replace_visitor =
     object
       inherit [_] map_statement as super
 
-      method! visit_Sequence env st1 st2 =
-        match st1.content with
-        | Loop _ ->
-            cassert __FILE__ __LINE__
-              (statement_has_no_loop_break_continue st2)
-              st2.span "Sequences of loops are not supported yet";
-            (replace_breaks_with st1 st2).content
-        | _ -> super#visit_Sequence env st1 st2
+      method! visit_statement env st =
+        match st.content with
+        | Sequence (st1, st2) -> begin
+            match st1.content with
+            | Loop _ ->
+                cassert __FILE__ __LINE__
+                  (statement_has_no_loop_break_continue st2)
+                  st2.span "Sequences of loops are not supported yet";
+                super#visit_statement env (replace_breaks_with st st2)
+            | Switch _ ->
+                (* This pushes st2 inside of the switch *)
+                super#visit_statement env (chain_statements st1 st2)
+            | _ -> super#visit_statement env st
+          end
+        | _ -> super#visit_statement env st
     end
   in
 
   (* Map  *)
   let body =
     match f.body with
-    | Some body -> Some { body with body = obj#visit_statement () body.body }
+    | Some body ->
+        Some { body with body = replace_visitor#visit_statement () body.body }
     | None -> None
   in
+
   let f = { f with body } in
   log#ldebug
     (lazy