Merge pull request #85 from AeneasVerif/son/fix_loops3

Fix some issues with the loops

1 files changed, 21 insertions, 5 deletions

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 22d176c9..fd3e334b 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -301,6 +301,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
   let parent_input_abs_ids =
     List.filter_map (fun x -> x) parent_input_abs_ids
   in
+  (* TODO: need to be careful for loops *)
+  assert (parent_input_abs_ids = []);
 
   (* Insert the return value in the return abstractions (by applying
    * borrow projections) *)
@@ -354,8 +356,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       let fun_abs_id =
         (RegionGroupId.nth inst_sg.regions_hierarchy back_id).id
       in
-      if not inside_loop then (fun_abs_id, true)
+      if not inside_loop then (Some fun_abs_id, true)
       else
+        (* We are inside a loop *)
         let pred (abs : abs) =
           match abs.kind with
           | Loop (_, rg_id', kind) ->
@@ -383,14 +386,24 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
              }
            ]}
         *)
-        let abs = Option.get (ctx_find_abs ctx pred) in
-        (abs.abs_id, false)
+        match ctx_find_abs ctx pred with
+        | None ->
+            (* The loop gives back nothing for this region group.
+               Ex.:
+               {[
+                 pub fn ignore_input_mut_borrow(_a: &mut u32) {
+                     loop {}
+                 }
+               ]}
+            *)
+            (None, false)
+        | Some abs -> (Some abs.abs_id, false)
     in
     log#ldebug
       (lazy
         ("evaluate_function_symbolic_synthesize_backward_from_return: ending \
           input abstraction: "
-        ^ AbstractionId.to_string current_abs_id));
+        ^ Print.option_to_string AbstractionId.to_string current_abs_id));
 
     (* Set the proper abstractions as endable *)
     let ctx =
@@ -427,7 +440,10 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       visit_loop_abs#visit_eval_ctx () ctx
     in
 
-    let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in
+    let current_abs_id =
+      match current_abs_id with None -> [] | Some id -> [ id ]
+    in
+    let target_abs_ids = List.append parent_input_abs_ids current_abs_id in
     let cf_end_target_abs cf =
       List.fold_left
         (fun cf id -> end_abstraction config id cf)