From 5581a065cc253b5c497c21edc3f8b681b978887d Mon Sep 17 00:00:00 2001
From: Emily Ong <emilyohq11@gmail.com>
Date: Sat, 3 Feb 2024 16:15:13 +0800
Subject: [PATCH 1/6] Allow unfolding of non-recursive predicates

---
 parsing/Pretty.ml                 | 13 ++++++++++++-
 parsing/core_lang.ml              |  3 ++-
 parsing/entail.ml                 | 16 +++++++++++-----
 parsing/hiplib.ml                 |  7 ++++++-
 parsing/hiptypes.ml               |  1 +
 parsing/subst.ml                  | 10 ++++++++++
 src/programs.t/test_new_entail.ml | 12 +++++++++++-
 7 files changed, 53 insertions(+), 9 deletions(-)

diff --git a/parsing/Pretty.ml b/parsing/Pretty.ml
index 2592c946..bbb490a5 100644
--- a/parsing/Pretty.ml
+++ b/parsing/Pretty.ml
@@ -413,7 +413,7 @@ let rec kappaToPure kappa : pi =
 
 
 
-let string_of_pred ({ p_name; p_params; p_body } : pred_def) : string =
+let string_of_pred ({ p_name; p_params; p_body; _ } : pred_def) : string =
   Format.asprintf "%s(%s) == %s" p_name (String.concat "," p_params) (string_of_spec_list p_body)
 
 let string_of_inclusion (lhs:spec list) (rhs:spec list) :string =
@@ -599,10 +599,21 @@ let is_just_res_of pi t =
 let lambda_to_pred_def name t =
   match t with
   | TLambda (_lid, params, spec, _body) ->
+    let find_rec p_name =
+      object(self)
+        inherit [_] reduce_spec as super
+        method zero = false
+        method plus = (||)
+    
+        method! visit_HigherOrder _ ((_p, _h, (f, _a), _r) as fn) =
+          self#plus (f = p_name) (super#visit_HigherOrder () fn)
+      end
+    in
     {
       p_name = name;
       p_params = params;
       p_body = spec;
+      p_rec = (find_rec name)#visit_disj_spec () spec;
     }
   | _ ->
     failwith
diff --git a/parsing/core_lang.ml b/parsing/core_lang.ml
index ffe2dce1..d4c415ae 100644
--- a/parsing/core_lang.ml
+++ b/parsing/core_lang.ml
@@ -480,7 +480,8 @@ let transform_str bound_names (s : structure_item) =
       | _ -> failwith (Format.asprintf "lemma %s should have function on the left" l_name)
     in
     Some (`Lem {l_name; l_params; l_left; l_right})
-  | Pstr_predicate (p_name, p_params, p_body) -> Some (`Pred {p_name; p_params; p_body})
+  | Pstr_predicate (p_name, p_params, p_body) ->
+    Some (`Pred {p_name; p_params; p_body; p_rec = (find_rec p_name)#visit_disj_spec () p_body})
   | Pstr_SL_predicate (p_sl_ex, p_sl_name, p_sl_params, p_sl_body) -> Some (`SLPred {p_sl_ex; p_sl_name; p_sl_params; p_sl_body})
 
   | Pstr_effect { peff_name; peff_kind=_; _ } ->
diff --git a/parsing/entail.ml b/parsing/entail.ml
index 42536b7b..4ff257d5 100644
--- a/parsing/entail.ml
+++ b/parsing/entail.ml
@@ -305,7 +305,7 @@ let instantiate_pred : pred_def -> term list -> term -> pred_def =
          (string_of_list (string_of_list string_of_staged_spec) bbody); *)
     bbody
   in
-  { pred with p_body }
+  { pred with p_body; p_rec = (find_rec pred.p_name)#visit_disj_spec () p_body }
 
 let rec unfold_predicate_aux pred prefix (s : spec) : disj_spec =
   match s with
@@ -587,8 +587,9 @@ and try_other_measures :
       (c1, res)
     with
     | Some (c1, def)
+      (* always allow unfolding of non-recursive predicates *)
       when List.length (List.filter (fun s -> s = (c1, `Left)) ctx.unfolded)
-           < unfolding_bound ->
+           < unfolding_bound || not def.p_rec ->
       let unf = unfold_predicate_norm "left" def s1 in
       let@ s1_1, ctx =
         all_state ~name:(Format.asprintf "unfold lhs: %s" c1)~to_s:string_of_normalisedStagedSpec ~init:ctx ~pivot:(fun c -> { ctx with subsumption_obl = c.subsumption_obl }) unf
@@ -607,8 +608,9 @@ and try_other_measures :
          (c2, res)
        with
       | Some (c2, pred_def)
+       (* always allow unfolding of non-recursive predicates *)
         when List.length (List.filter (fun s -> s = (c2, `Right)) ctx.unfolded)
-             < unfolding_bound ->
+             < unfolding_bound || not pred_def.p_rec ->
         let unf = unfold_predicate_norm "right" pred_def s2 in
         let@ s2_1 =
           any ~name:(Format.asprintf "unfold rhs: %s" c2)~to_s:string_of_normalisedStagedSpec unf
@@ -912,8 +914,12 @@ let derive_predicate m_name m_params disj =
     List.map (fun (effs, (vs, pre, (p, h))) -> (effs, (vs, pre, (p, h)))) norm
     |> List.map normalisedStagedSpec2Spec
   in
-  let res =
-    { p_name = m_name; p_params = m_params @ ["res"] ; p_body = new_spec } (* ASK Darius *)
+  let res = {
+    p_name = m_name;
+    p_params = m_params @ ["res"];
+    p_body = new_spec;
+    p_rec = (find_rec m_name)#visit_disj_spec () new_spec
+  } (* ASK Darius *)
   in
   debug ~at:2
     ~title:(Format.asprintf "derive predicate %s" m_name)
diff --git a/parsing/hiplib.ml b/parsing/hiplib.ml
index d9dc236e..d8427976 100644
--- a/parsing/hiplib.ml
+++ b/parsing/hiplib.ml
@@ -978,7 +978,12 @@ let process_items (strs: structure_item list) : unit =
         let body' = replaceSLPredicatesWithDef p.p_body prog.cp_sl_predicates in 
         (*print_endline ("~~~> " ^ string_of_disj_spec body');
         *)
-        let (p': pred_def) = {p_name =p.p_name; p_params = p.p_params; p_body = body'} in 
+        let (p': pred_def) = {
+          p_name = p.p_name;
+          p_params = p.p_params;
+          p_body = body';
+          p_rec = (find_rec p.p_name)#visit_disj_spec () body';
+        } in 
         bound_names, { prog with cp_predicates = SMap.add p'.p_name p' prog.cp_predicates }
 
       | Some (`SLPred p) -> 
diff --git a/parsing/hiptypes.ml b/parsing/hiptypes.ml
index 44673cb7..b97753c8 100644
--- a/parsing/hiptypes.ml
+++ b/parsing/hiptypes.ml
@@ -290,6 +290,7 @@ type pred_def = {
   p_name: string;
   p_params: string list; (* list to ensure ordering. last param is typically a return value *)
   p_body: disj_spec;
+  p_rec: bool;
 }
 
 type sl_pred_def = {
diff --git a/parsing/subst.ml b/parsing/subst.ml
index a4f4d1de..67622265 100644
--- a/parsing/subst.ml
+++ b/parsing/subst.ml
@@ -277,3 +277,13 @@ let quantify_res_state (p, h) =
 
   let contains_res_state (p, h) =
     SSet.mem "res" (used_vars_state (p, h))
+
+let find_rec p_name =
+  object(self)
+    inherit [_] reduce_spec as super
+    method zero = false
+    method plus = (||)
+
+    method! visit_HigherOrder _ ((_p, _h, (f, _a), _r) as fn) =
+      self#plus (f = p_name) (super#visit_HigherOrder () fn)
+  end
diff --git a/src/programs.t/test_new_entail.ml b/src/programs.t/test_new_entail.ml
index 75eb69a6..748cc874 100644
--- a/src/programs.t/test_new_entail.ml
+++ b/src/programs.t/test_new_entail.ml
@@ -286,4 +286,14 @@ let call_f_in_g ()
 (*@ ens res=5 @*)
 = let x = 3 in
   let f x = x in
-  f 5
\ No newline at end of file
+  f 5
+
+let call_ret f (* ex v; f(100,v); ens res=v *) =
+  f 100
+
+let test_non_rec_pred ()
+(*@ ens res=100 @*)
+= let id i = i in
+  id 2;
+
+  call_ret id
\ No newline at end of file

From a74f2f9dff847b1a0db476d47e82328595c88600 Mon Sep 17 00:00:00 2001
From: Emily Ong <emilyohq11@gmail.com>
Date: Sat, 3 Feb 2024 16:16:29 +0800
Subject: [PATCH 2/6] Check why3 only for Prusti's all example

---
 src/programs.t/run.t | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/programs.t/run.t b/src/programs.t/run.t
index cf90c7ed..614d134a 100644
--- a/src/programs.t/run.t
+++ b/src/programs.t/run.t
@@ -95,7 +95,7 @@ ALL OK!
   $ check ../examples/exception.ml
   ALL OK!
 
-  $ check ../prusti/all.ml
+  $ check_why3_only ../prusti/all.ml
   ALL OK!
 
   $ check ../prusti/blameassgn.ml

From 21e68961cd3d0ebe318c2434a9fb954d034cdb52 Mon Sep 17 00:00:00 2001
From: Emily Ong <emilyohq11@gmail.com>
Date: Wed, 7 Feb 2024 16:34:47 +0800
Subject: [PATCH 3/6] Remove unneeded visit and fix nits

---
 parsing/Pretty.ml                 | 19 +++++++++----------
 parsing/entail.ml                 |  2 +-
 parsing/subst.ml                  | 10 ----------
 src/examples/{later => }/calls.ml | 10 +++++-----
 src/programs.t/run.t              |  3 +++
 src/programs.t/test_new_entail.ml |  2 +-
 6 files changed, 19 insertions(+), 27 deletions(-)
 rename src/examples/{later => }/calls.ml (88%)

diff --git a/parsing/Pretty.ml b/parsing/Pretty.ml
index bbb490a5..3c954b5b 100644
--- a/parsing/Pretty.ml
+++ b/parsing/Pretty.ml
@@ -364,6 +364,15 @@ let rec existPi pi li =
     )
     ;;
 
+let find_rec p_name =
+  object(self)
+    inherit [_] reduce_spec as super
+    method zero = false
+    method plus = (||)
+
+    method! visit_HigherOrder _ ((_p, _h, (f, _a), _r) as fn) =
+      self#plus (f = p_name) (super#visit_HigherOrder () fn)
+  end    
 
 (**********************************************)
 exception FooAskz3 of string
@@ -599,16 +608,6 @@ let is_just_res_of pi t =
 let lambda_to_pred_def name t =
   match t with
   | TLambda (_lid, params, spec, _body) ->
-    let find_rec p_name =
-      object(self)
-        inherit [_] reduce_spec as super
-        method zero = false
-        method plus = (||)
-    
-        method! visit_HigherOrder _ ((_p, _h, (f, _a), _r) as fn) =
-          self#plus (f = p_name) (super#visit_HigherOrder () fn)
-      end
-    in
     {
       p_name = name;
       p_params = params;
diff --git a/parsing/entail.ml b/parsing/entail.ml
index 4ff257d5..81ee485d 100644
--- a/parsing/entail.ml
+++ b/parsing/entail.ml
@@ -305,7 +305,7 @@ let instantiate_pred : pred_def -> term list -> term -> pred_def =
          (string_of_list (string_of_list string_of_staged_spec) bbody); *)
     bbody
   in
-  { pred with p_body; p_rec = (find_rec pred.p_name)#visit_disj_spec () p_body }
+  { pred with p_body }
 
 let rec unfold_predicate_aux pred prefix (s : spec) : disj_spec =
   match s with
diff --git a/parsing/subst.ml b/parsing/subst.ml
index 67622265..a4f4d1de 100644
--- a/parsing/subst.ml
+++ b/parsing/subst.ml
@@ -277,13 +277,3 @@ let quantify_res_state (p, h) =
 
   let contains_res_state (p, h) =
     SSet.mem "res" (used_vars_state (p, h))
-
-let find_rec p_name =
-  object(self)
-    inherit [_] reduce_spec as super
-    method zero = false
-    method plus = (||)
-
-    method! visit_HigherOrder _ ((_p, _h, (f, _a), _r) as fn) =
-      self#plus (f = p_name) (super#visit_HigherOrder () fn)
-  end
diff --git a/src/examples/later/calls.ml b/src/examples/calls.ml
similarity index 88%
rename from src/examples/later/calls.ml
rename to src/examples/calls.ml
index 8bc87f5e..268d0add 100644
--- a/src/examples/later/calls.ml
+++ b/src/examples/calls.ml
@@ -3,7 +3,7 @@ let call_ret f =
   f 100
 
 let main_false ()
-(*@ Norm(emp, 2) @*)
+(*@ ens res=2 @*)
 = let x = ref 0 in
   let swap i = 
     let r = !x in 
@@ -18,7 +18,7 @@ let main_false ()
   call_ret swap
 
 let main ()
-(*@ Norm(emp, 2) @*)
+(*@ ens res=2 @*)
 = let x = ref 0 in
   let swap i = 
     let r = !x in 
@@ -33,7 +33,7 @@ let main ()
   call_ret swap
 
 let main1_false ()
-(*@ Norm(emp, 1) @*)
+(*@ ens res=1 @*)
 = let x = ref 2 in
 
   let swap i =
@@ -49,7 +49,7 @@ let main1_false ()
   1
 
 let main3_false ()
-(*@ Norm(emp, 1) @*)
+(*@ ens res=1 @*)
 = let x = ref 2 in
   assert (!x=2);
   x := !x + 1;
@@ -57,7 +57,7 @@ let main3_false ()
   1
 
 let main4_false ()
-(*@ Norm(emp, 1) @*)
+(*@ ens res=1 @*)
 = let x = ref 2 in
   assert (!x=2);
   x := 3;
diff --git a/src/programs.t/run.t b/src/programs.t/run.t
index 614d134a..641d4ae9 100644
--- a/src/programs.t/run.t
+++ b/src/programs.t/run.t
@@ -83,6 +83,9 @@ ALL OK!
   $ check ../examples/length.ml
   ALL OK!
 
+  $ check ../examples/calls.ml
+  ALL OK!
+
   $ check ../examples/closure.ml
   ALL OK!
 
diff --git a/src/programs.t/test_new_entail.ml b/src/programs.t/test_new_entail.ml
index 748cc874..c5a7e382 100644
--- a/src/programs.t/test_new_entail.ml
+++ b/src/programs.t/test_new_entail.ml
@@ -296,4 +296,4 @@ let test_non_rec_pred ()
 = let id i = i in
   id 2;
 
-  call_ret id
\ No newline at end of file
+  call_ret id

From c7642d1bc3a510dbca71b615de64fe7716eaea8b Mon Sep 17 00:00:00 2001
From: Emily Ong <emilyohq11@gmail.com>
Date: Wed, 7 Feb 2024 16:36:02 +0800
Subject: [PATCH 4/6] Remove false

---
 src/examples/calls.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/examples/calls.ml b/src/examples/calls.ml
index 268d0add..01da8327 100644
--- a/src/examples/calls.ml
+++ b/src/examples/calls.ml
@@ -32,7 +32,7 @@ let main ()
   (* L2: the call here is only valid after L1*)
   call_ret swap
 
-let main1_false ()
+let main1 ()
 (*@ ens res=1 @*)
 = let x = ref 2 in
 
@@ -48,7 +48,7 @@ let main1_false ()
   (* the function call is only valid at the first time *)
   1
 
-let main3_false ()
+let main3 ()
 (*@ ens res=1 @*)
 = let x = ref 2 in
   assert (!x=2);

From f92b4ec03559c81d5b4da31190ccc44525b2f0e4 Mon Sep 17 00:00:00 2001
From: Emily Ong <emilyohq11@gmail.com>
Date: Tue, 20 Feb 2024 21:39:38 +0800
Subject: [PATCH 5/6] Check atomics for names

---
 parsing/Pretty.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/parsing/Pretty.ml b/parsing/Pretty.ml
index 3c954b5b..69d1e526 100644
--- a/parsing/Pretty.ml
+++ b/parsing/Pretty.ml
@@ -372,6 +372,11 @@ let find_rec p_name =
 
     method! visit_HigherOrder _ ((_p, _h, (f, _a), _r) as fn) =
       self#plus (f = p_name) (super#visit_HigherOrder () fn)
+
+    method! visit_Atomic () op a b =
+      match op with
+      | EQ -> (string_of_term a) = p_name || (string_of_term b) = p_name
+      | _ -> false
   end    
 
 (**********************************************)

From 1cb721f4b5f585f7c6e656ff434f3669ca203f47 Mon Sep 17 00:00:00 2001
From: Emily Ong <emilyohq11@gmail.com>
Date: Tue, 20 Feb 2024 21:52:08 +0800
Subject: [PATCH 6/6] Remove redundant string call

---
 parsing/Pretty.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/parsing/Pretty.ml b/parsing/Pretty.ml
index 69d1e526..658bf2c6 100644
--- a/parsing/Pretty.ml
+++ b/parsing/Pretty.ml
@@ -375,7 +375,9 @@ let find_rec p_name =
 
     method! visit_Atomic () op a b =
       match op with
-      | EQ -> (string_of_term a) = p_name || (string_of_term b) = p_name
+      | EQ -> (match (a, b) with
+        | (Var x, Var y) -> x = p_name || y = p_name
+        | _ -> false)
       | _ -> false
   end