Allow unfolding of basic non-recursive predicates

parsing/Pretty.ml

@@ -364,6 +364,22 @@ 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)
+
+    method! visit_Atomic () op a b =
+      match op with
+      | EQ -> (match (a, b) with
+        | (Var x, Var y) -> x = p_name || y = p_name
+        | _ -> false)
+      | _ -> false
+  end    
 
 (**********************************************)
 exception FooAskz3 of string
@@ -413,7 +429,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 =
@@ -603,6 +619,7 @@ let lambda_to_pred_def name t =
       p_name = name;
       p_params = params;
       p_body = spec;
+      p_rec = (find_rec name)#visit_disj_spec () spec;
     }
   | _ ->
     failwith

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=_; _ } ->

parsing/entail.ml

@@ -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)

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) -> 

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 = {

src/examples/later/calls.ml → 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 
@@ -32,8 +32,8 @@ let main ()
   (* L2: the call here is only valid after L1*)
   call_ret swap
 
-let main1_false ()
-(*@ Norm(emp, 1) @*)
+let main1 ()
+(*@ ens res=1 @*)
 = let x = ref 2 in
 
   let swap i =
@@ -48,16 +48,16 @@ let main1_false ()
   (* the function call is only valid at the first time *)
   1
 
-let main3_false ()
-(*@ Norm(emp, 1) @*)
+let main3 ()
+(*@ ens res=1 @*)
 = let x = ref 2 in
   assert (!x=2);
   x := !x + 1;
   assert (!x=4);
   1
 
 let main4_false ()
-(*@ Norm(emp, 1) @*)
+(*@ ens res=1 @*)
 = let x = ref 2 in
   assert (!x=2);
   x := 3;

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!
 
@@ -95,7 +98,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

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
+  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