add consume & produce commands (#309)

Signed-off-by: Sacha Ayoun <[email protected]>

GillianCore/GIL_Syntax/Gil_syntax.mli

@@ -671,6 +671,8 @@ module SLCmd : sig
     | ApplyLem of string * Expr.t list * string list  (** Apply lemma *)
     | SepAssert of Asrt.t * string list  (** Assert *)
     | Invariant of Asrt.t * string list  (** Invariant *)
+    | Consume of Asrt.t * string list
+    | Produce of Asrt.t
     | SymbExec
 
   (** @deprecated Use {!Visitors.endo} instead *)
@@ -1374,6 +1376,8 @@ module Visitors : sig
          ; visit_Int : 'c -> Literal.t -> Z.t -> Literal.t
          ; visit_IntType : 'c -> Type.t -> Type.t
          ; visit_Invariant : 'c -> SLCmd.t -> Asrt.t -> string list -> SLCmd.t
+         ; visit_Consume : 'c -> SLCmd.t -> Asrt.t -> string list -> SLCmd.t
+         ; visit_Produce : 'c -> SLCmd.t -> Asrt.t -> SLCmd.t
          ; visit_LAction :
              'c -> 'f Cmd.t -> string -> string -> Expr.t list -> 'f Cmd.t
          ; visit_LList : 'c -> Literal.t -> Literal.t list -> Literal.t
@@ -1640,6 +1644,8 @@ module Visitors : sig
     method visit_Int : 'c -> Literal.t -> Z.t -> Literal.t
     method visit_IntType : 'c -> Type.t -> Type.t
     method visit_Invariant : 'c -> SLCmd.t -> Asrt.t -> string list -> SLCmd.t
+    method visit_Consume : 'c -> SLCmd.t -> Asrt.t -> string list -> SLCmd.t
+    method visit_Produce : 'c -> SLCmd.t -> Asrt.t -> SLCmd.t
 
     method visit_LAction :
       'c -> 'f Cmd.t -> string -> string -> Expr.t list -> 'f Cmd.t
@@ -1906,6 +1912,8 @@ module Visitors : sig
          ; visit_GuardedGoto : 'c -> Expr.t -> 'g -> 'g -> 'f
          ; visit_If : 'c -> Expr.t -> LCmd.t list -> LCmd.t list -> 'f
          ; visit_Invariant : 'c -> Asrt.t -> string list -> 'f
+         ; visit_Consume : 'c -> Asrt.t -> string list -> 'f
+         ; visit_Produce : 'c -> Asrt.t -> 'f
          ; visit_LAction : 'c -> string -> string -> Expr.t list -> 'f
          ; visit_LList : 'c -> Literal.t list -> 'f
          ; visit_LVar : 'c -> LVar.t -> 'f
@@ -2142,6 +2150,8 @@ module Visitors : sig
     method visit_GuardedGoto : 'c -> Expr.t -> 'g -> 'g -> 'f
     method visit_If : 'c -> Expr.t -> LCmd.t list -> LCmd.t list -> 'f
     method visit_Invariant : 'c -> Asrt.t -> string list -> 'f
+    method visit_Consume : 'c -> Asrt.t -> string list -> 'f
+    method visit_Produce : 'c -> Asrt.t -> 'f
     method visit_LAction : 'c -> string -> string -> Expr.t list -> 'f
     method visit_LList : 'c -> Literal.t list -> 'f
     method visit_LVar : 'c -> LVar.t -> 'f
@@ -2390,6 +2400,8 @@ module Visitors : sig
          ; visit_Int : 'c -> Z.t -> unit
          ; visit_IntType : 'c -> unit
          ; visit_Invariant : 'c -> Asrt.t -> string list -> unit
+         ; visit_Consume : 'c -> Asrt.t -> string list -> unit
+         ; visit_Produce : 'c -> Asrt.t -> unit
          ; visit_LAction : 'c -> string -> string -> Expr.t list -> unit
          ; visit_LList : 'c -> Literal.t list -> unit
          ; visit_LVar : 'c -> string -> unit
@@ -2630,6 +2642,8 @@ module Visitors : sig
     method visit_Int : 'c -> Z.t -> unit
     method visit_IntType : 'c -> unit
     method visit_Invariant : 'c -> Asrt.t -> string list -> unit
+    method visit_Consume : 'c -> Asrt.t -> string list -> unit
+    method visit_Produce : 'c -> Asrt.t -> unit
     method visit_LAction : 'c -> string -> string -> Expr.t list -> unit
     method visit_LList : 'c -> Literal.t list -> unit
     method visit_LVar : 'c -> string -> unit

GillianCore/GIL_Syntax/SLCmd.ml

@@ -19,6 +19,10 @@ type t = TypeDef__.slcmd =
   | ApplyLem of string * Expr.t list * string list  (** Apply lemma      *)
   | SepAssert of Asrt.t * string list  (** Assert           *)
   | Invariant of Asrt.t * string list  (** Invariant        *)
+  | Consume of
+      Asrt.t
+      * string list (* Consumes an assertion. Warning, not frame-preserving *)
+  | Produce of Asrt.t (* Produces an assertion. Warning, not frame-preserving *)
   | SymbExec
 [@@deriving yojson]
 
@@ -47,6 +51,8 @@ let map
   | ApplyLem (s, l, existentials) -> ApplyLem (s, List.map map_e l, existentials)
   | SepAssert (a, binders) -> SepAssert (map_a a, binders)
   | Invariant (a, existentials) -> Invariant (map_a a, existentials)
+  | Consume (a, binders) -> Consume (map_a a, binders)
+  | Produce a -> Produce (map_a a)
   | SymbExec -> SymbExec
   | Package { lhs = lname, largs; rhs = rname, rargs } ->
       Package
@@ -64,7 +70,8 @@ let pvars (slcmd : t) : SS.t =
   | GUnfold _ -> SS.empty
   | Package { lhs = _, les1; rhs = _, les2 } ->
       SS.union (pvars_es les1) (pvars_es les2)
-  | SepAssert (a, _) | Invariant (a, _) -> Asrt.pvars a
+  | SepAssert (a, _) | Invariant (a, _) | Consume (a, _) | Produce a ->
+      Asrt.pvars a
   | SymbExec -> SS.empty
 
 let lvars (slcmd : t) : SS.t =
@@ -84,8 +91,9 @@ let lvars (slcmd : t) : SS.t =
       SS.union (lvars_es les1) (lvars_es les2)
   | ApplyLem (_, es, _) -> lvars_es es
   | GUnfold _ -> SS.empty
-  | SepAssert (a, binders) -> SS.union (Asrt.lvars a) (SS.of_list binders)
-  | Invariant (a, _) -> Asrt.lvars a
+  | SepAssert (a, binders) | Consume (a, binders) ->
+      SS.union (Asrt.lvars a) (SS.of_list binders)
+  | Invariant (a, _) | Produce a -> Asrt.lvars a
   | SymbExec -> SS.empty
 
 let locs (slcmd : t) : SS.t =
@@ -105,7 +113,8 @@ let locs (slcmd : t) : SS.t =
       SS.union (locs_es les1) (locs_es les2)
   | ApplyLem (_, es, _) -> locs_es es
   | GUnfold _ -> SS.empty
-  | SepAssert (a, _) | Invariant (a, _) -> Asrt.locs a
+  | SepAssert (a, _) | Invariant (a, _) | Consume (a, _) | Produce a ->
+      Asrt.locs a
   | SymbExec -> SS.empty
 
 let pp_folding_info =
@@ -149,6 +158,9 @@ let pp fmt lcmd =
   | SepAssert (a, binders) ->
       Fmt.pf fmt "@[sep_assert %a %a@]" (Fmt.parens Asrt.pp) a pp_binders
         binders
+  | Consume (a, binders) ->
+      Fmt.pf fmt "@[consume %a %a@]" (Fmt.parens Asrt.pp) a pp_binders binders
+  | Produce a -> Fmt.pf fmt "@[produce %a@]" (Fmt.parens Asrt.pp) a
   | Invariant (a, existentials) ->
       let pp_exs f exs =
         match exs with

GillianCore/GIL_Syntax/TypeDef__.ml

@@ -182,6 +182,8 @@ and slcmd =
   | ApplyLem of string * expr list * string list
   | SepAssert of assertion * string list
   | Invariant of assertion * string list
+  | Consume of assertion * string list
+  | Produce of assertion
   | SymbExec
 
 and lcmd =

GillianCore/engine/Abstraction/PState.ml

@@ -412,6 +412,170 @@ module Make (State : SState.S) :
       preds_list;
     { state; preds; wands = Wands.init []; pred_defs; variants }
 
+  let consume ~(prog : 'a MP.prog) astate a binders =
+    if not (List.for_all Names.is_lvar_name binders) then
+      failwith "Binding of pure variables in *-assert.";
+    let store = State.get_store astate.state in
+    let pvars_store = SStore.domain store in
+    let pvars_a = Asrt.pvars a in
+    let pvars_diff = SS.diff pvars_a pvars_store in
+    (if not (SS.is_empty pvars_diff) then
+       let pvars_errs : err_t list =
+         List.map (fun pvar : err_t -> EVar pvar) (SS.elements pvars_diff)
+       in
+       raise (Internal_State_Error (pvars_errs, astate)));
+    let store_subst = SStore.to_ssubst store in
+    let a = SVal.SESubst.substitute_asrt store_subst ~partial:true a in
+    (* let known_vars   = SS.diff (SS.filter is_spec_var_name (Asrt.lvars a)) (SS.of_list binders) in *)
+    let state_lvars = State.get_lvars astate.state in
+    let known_lvars =
+      SS.elements
+        (SS.diff (SS.inter state_lvars (Asrt.lvars a)) (SS.of_list binders))
+    in
+    let known_lvars = List.map (fun x -> Expr.LVar x) known_lvars in
+    let asrt_alocs =
+      List.map (fun x -> Expr.ALoc x) (SS.elements (Asrt.alocs a))
+    in
+    let known_matchables = Expr.Set.of_list (known_lvars @ asrt_alocs) in
+
+    let pred_ins =
+      Hashtbl.fold
+        (fun name (pred : Pred.t) pred_ins ->
+          Hashtbl.add pred_ins name pred.pred_ins;
+          pred_ins)
+        prog.prog.preds
+        (Hashtbl.create Config.medium_tbl_size)
+    in
+
+    let mp =
+      MP.init known_matchables Expr.Set.empty pred_ins [ (a, (None, None)) ]
+    in
+    let vars_to_forget = SS.inter state_lvars (SS.of_list binders) in
+    if not (SS.is_empty vars_to_forget) then (
+      let oblivion_subst = fresh_subst vars_to_forget in
+      L.verbose (fun m ->
+          m "Forget @[%a@] with subst: %a"
+            Fmt.(iter ~sep:comma SS.iter string)
+            vars_to_forget SVal.SESubst.pp oblivion_subst);
+
+      (* TODO: THIS SUBST IN PLACE MUST NOT BRANCH *)
+      let subst_in_place = substitution_in_place oblivion_subst astate in
+      assert (List.length subst_in_place = 1);
+      let astate = List.hd subst_in_place in
+
+      L.verbose (fun m -> m "State after substitution:@\n@[%a@]\n" pp astate));
+    let mp =
+      match mp with
+      | Error asrts -> raise (Preprocessing_Error [ MPAssert (a, asrts) ])
+      | Ok mp -> mp
+    in
+    let bindings =
+      List.map
+        (fun (e : Expr.t) ->
+          let id =
+            match e with
+            | LVar _ | ALoc _ -> e
+            | _ ->
+                raise (Failure "Impossible: matchable not an lvar or an aloc")
+          in
+          (id, e))
+        (Expr.Set.elements known_matchables)
+    in
+    (* let old_astate = copy astate in *)
+    let subst = SVal.SESubst.init bindings in
+    let open Syntaxes.List in
+    let* matching_result = SMatcher.match_ astate subst mp LogicCommand in
+    match matching_result with
+    | Ok (new_state, subst', _) ->
+        (* Successful matching *)
+        let lbinders = List.map (fun x -> Expr.LVar x) binders in
+        let new_bindings =
+          List.map (fun e -> (e, SVal.SESubst.get subst' e)) lbinders
+        in
+        let success = List.for_all (fun (_, x_v) -> x_v <> None) new_bindings in
+        if not success then
+          raise (Failure "Assert failed - binders not captured");
+        let additional_bindings =
+          List.filter
+            (fun (e, v) -> (not (List.mem e lbinders)) && not (Expr.equal e v))
+            (SVal.SESubst.to_list subst')
+        in
+        let new_bindings =
+          List.map (fun (x, y) -> (x, Option.get y)) new_bindings
+          @ additional_bindings
+        in
+        let new_bindings =
+          List.map (fun (e, e_v) -> Asrt.Pure (Eq (e, e_v))) new_bindings
+        in
+        let a_new_bindings = Asrt.star new_bindings in
+        let full_subst = make_id_subst a in
+        let a_produce = a_new_bindings in
+        let open Res_list.Syntax in
+        let result =
+          let** new_astate = SMatcher.produce new_state full_subst a_produce in
+          let new_state' =
+            State.add_spec_vars new_astate.state (SS.of_list binders)
+          in
+          let subst, new_states =
+            State.simplify ~kill_new_lvars:true new_state'
+          in
+          let () = Preds.substitution_in_place subst new_astate.preds in
+          let () = Wands.substitution_in_place subst new_astate.wands in
+          let+ new_state = new_states in
+          Ok (copy_with_state new_astate new_state)
+        in
+        Res_list.map_error
+          (fun _ ->
+            let msg =
+              Fmt.str
+                "Assert failed with argument %a. unable to produce variable \
+                 bindings."
+                Asrt.pp a
+            in
+            StateErr.EOther msg)
+          result
+    | Error err ->
+        let fail_pfs : Formula.t = State.get_failing_constraint err in
+
+        let failing_model = State.sat_check_f astate.state [ fail_pfs ] in
+        let msg =
+          Fmt.str
+            "Assert failed with argument @[<h>%a@]. matching failed.@\n\
+             @[<v 2>Errors:@\n\
+             %a.@]@\n\
+             @[<v 2>Failing Model:@\n\
+             %a@]@\n"
+            Asrt.pp a State.pp_err err
+            Fmt.(option ~none:(any "CANNOT CREATE MODEL") SVal.SESubst.pp)
+            failing_model
+        in
+        L.print_to_all msg;
+        Res_list.error_with (StateErr.EPure fail_pfs)
+
+  let produce astate a =
+    let store = State.get_store astate.state in
+    let pvars_store = SStore.domain store in
+    let pvars_a = Asrt.pvars a in
+    let pvars_diff = SS.diff pvars_a pvars_store in
+    (if not (SS.is_empty pvars_diff) then
+       let pvars_errs : err_t list =
+         List.map (fun pvar : err_t -> EVar pvar) (SS.elements pvars_diff)
+       in
+       raise (Internal_State_Error (pvars_errs, astate)));
+    let store_subst = SStore.to_ssubst store in
+    let a = SVal.SESubst.substitute_asrt store_subst ~partial:true a in
+    let open Syntaxes.List in
+    let open Res_list.Syntax in
+    let full_subst = make_id_subst a in
+    let** new_astate = SMatcher.produce astate full_subst a in
+    let subst, new_states =
+      State.simplify ~kill_new_lvars:true new_astate.state
+    in
+    let () = Preds.substitution_in_place subst new_astate.preds in
+    let () = Wands.substitution_in_place subst new_astate.wands in
+    let+ new_state = new_states in
+    Ok (copy_with_state new_astate new_state)
+
   let match_invariant
       (prog : 'a MP.prog)
       (revisited : bool)
@@ -902,6 +1066,8 @@ module Make (State : SState.S) :
               in
               L.print_to_all msg;
               Res_list.error_with (StateErr.EPure fail_pfs))
+      | Consume (asrt, binders) -> consume ~prog astate asrt binders
+      | Produce asrt -> produce astate asrt
       | ApplyLem (lname, args, binders) ->
           if not (List.for_all Names.is_lvar_name binders) then
             failwith "Binding of pure variables in lemma application.";

GillianCore/gil_parser/GIL_Lexer.mll

@@ -111,6 +111,8 @@
         "else",         GIL_Parser.LELSE;
         "macro",        GIL_Parser.MACRO;
         "invariant",    GIL_Parser.INVARIANT;
+        "consume",      GIL_Parser.CONSUME;
+        "produce",      GIL_Parser.PRODUCE;
         "assert",       GIL_Parser.ASSERT;
         "assume",       GIL_Parser.ASSUME;
         "assume_type",  GIL_Parser.ASSUME_TYPE;

GillianCore/gil_parser/GIL_Parser.mly

@@ -129,6 +129,8 @@ let normalised_lvar_r = Str.regexp "##NORMALISED_LVAR"
 %token ASSERT
 %token SEPASSERT
 %token INVARIANT
+%token CONSUME 
+%token PRODUCE
 %token ASSUME_TYPE
 %token LSTNTH
 %token LSTREPEAT
@@ -763,6 +765,12 @@ g_logic_cmd_target:
 (* invariant (a) [existentials: x, y, z] *)
   | INVARIANT; LBRACE; a = g_assertion_target; RBRACE; binders = option(binders_target)
     { LCmd.SL (Invariant (a, Option.value ~default:[ ] binders)) }
+
+  | CONSUME; LBRACE; a = g_assertion_target; RBRACE; binders = option(binders_target)
+    { LCmd.SL (Consume (a, Option.value ~default:[ ] binders)) }
+
+  | PRODUCE; LBRACE; a = g_assertion_target; RBRACE;
+    { LCmd.SL (Produce a) }
 
 (* assert_* (a) [bind: x, y, z] *)
   | SEPASSERT; LBRACE; a = g_assertion_target; RBRACE; binders = option(binders_target)