forall exprs (#295)

* add EForall to expression AST

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

* Don't crash when reducing || or && and one of the sides can't be reduced.

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

---------

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

GillianCore/GIL_Syntax/Expr.ml

@@ -14,6 +14,7 @@ type t = TypeDef__.expr =
   | ESet of t list  (** Sets of expressions     *)
   | Exists of (string * Type.t option) list * t
       (** Existential quantification. This is now a circus because the separation between Formula and Expr doesn't make sense anymore. *)
+  | EForall of (string * Type.t option) list * t
 [@@deriving eq, ord]
 
 let to_yojson = TypeDef__.expr_to_yojson
@@ -317,6 +318,10 @@ let rec map_opt
             match map_e e with
             | Some e' -> Some (Exists (bt, e'))
             | _ -> None)
+        | EForall (bt, e) -> (
+            match map_e e with
+            | Some e' -> Some (EForall (bt, e'))
+            | _ -> None)
       in
       Option.map f_after mapped_expr
 
@@ -349,6 +354,10 @@ let rec pp fmt e =
       Fmt.pf fmt "(exists %a . %a)"
         (Fmt.list ~sep:Fmt.comma pp_var_with_type)
         bt pp e
+  | EForall (bt, e) ->
+      Fmt.pf fmt "(forall %a . %a)"
+        (Fmt.list ~sep:Fmt.comma pp_var_with_type)
+        bt pp e
 
 let rec full_pp fmt e =
   match e with
@@ -409,7 +418,7 @@ let rec is_concrete (le : t) : bool =
 
   match le with
   | Lit _ | PVar _ -> true
-  | LVar _ | ALoc _ | Exists _ -> false
+  | LVar _ | ALoc _ | Exists _ | EForall _ -> false
   | UnOp (_, e) -> loop [ e ]
   | BinOp (e1, _, e2) -> loop [ e1; e2 ]
   | LstSub (e1, e2, e3) -> loop [ e1; e2; e3 ]

GillianCore/GIL_Syntax/Formula.ml

@@ -244,6 +244,7 @@ let pp = pp_parametric Expr.pp
 let full_pp = pp_parametric Expr.full_pp
 
 let rec lift_logic_expr (e : Expr.t) : (t * t) option =
+  let open Syntaxes.Option in
   let f = lift_logic_expr in
   match e with
   | LVar _ | PVar _ -> Some (Eq (e, Lit (Bool true)), Eq (e, Lit (Bool false)))
@@ -273,16 +274,27 @@ let rec lift_logic_expr (e : Expr.t) : (t * t) option =
   | BinOp (e1, BSetSub, e2) ->
       let a = SetSub (e1, e2) in
       Some (a, Not a)
-  | BinOp (e1, BAnd, e2) -> (
-      match (f e1, f e2) with
-      | Some (a1, na1), Some (a2, na2) -> Some (And (a1, a2), Or (na1, na2))
-      | _ -> None)
-  | BinOp (e1, BOr, e2) -> (
-      match (f e1, f e2) with
-      | Some (a1, na1), Some (a2, na2) -> Some (Or (a1, a2), And (na1, na2))
-      | _ -> None)
-  | UnOp (UNot, e') -> Option.map (fun (a, na) -> (na, a)) (f e')
-  | Exists _ as e -> Some (Eq (e, Expr.bool true), Eq (e, Expr.bool false))
+  | BinOp (e1, BAnd, e2) ->
+      let* a1, na1 = f e1 in
+      let+ a2, na2 = f e2 in
+      (And (a1, a2), Or (na1, na2))
+  | BinOp (e1, BOr, e2) ->
+      let* a1, na1 = f e1 in
+      let+ a2, na2 = f e2 in
+      (Or (a1, a2), And (na1, na2))
+  | UnOp (UNot, e') ->
+      let+ a, na = f e' in
+      (na, a)
+  | Exists (bt, inner) as e ->
+      let+ _, inner_neg = f inner in
+      let neg = ForAll (bt, inner_neg) in
+      (Eq (e, Expr.bool true), neg)
+  | EForall (bt, e) ->
+      let+ inner, _ = f e in
+      let pos = ForAll (bt, inner) in
+      let inner_neg = Expr.Infix.not e in
+      let neg = Expr.Exists (bt, inner_neg) in
+      (pos, Eq (neg, Expr.bool true))
   | _ -> None
 
 let rec to_expr (a : t) : Expr.t option =

GillianCore/GIL_Syntax/Gil_syntax.mli

@@ -260,6 +260,7 @@ module Expr : sig
     | ESet of t list  (** Sets of expressions *)
     | Exists of (string * Type.t option) list * t
         (** Existential quantification. This is now a circus because the separation between Formula and Expr doesn't make sense anymore. *)
+    | EForall of (string * Type.t option) list * t
   [@@deriving yojson]
 
   (** {2: Helpers for building expressions}
@@ -1315,6 +1316,8 @@ module Visitors : sig
          ; visit_ESet : 'c -> Expr.t -> Expr.t list -> Expr.t
          ; visit_Exists :
              'c -> Expr.t -> (string * Type.t option) list -> Expr.t -> Expr.t
+         ; visit_EForall :
+             'c -> Expr.t -> (string * Type.t option) list -> Expr.t -> Expr.t
          ; visit_Emp : 'c -> Asrt.t -> Asrt.t
          ; visit_Empty : 'c -> Literal.t -> Literal.t
          ; visit_EmptyType : 'c -> Type.t -> Type.t
@@ -1578,6 +1581,9 @@ module Visitors : sig
     method visit_Exists :
       'c -> Expr.t -> (string * Type.t option) list -> Expr.t -> Expr.t
 
+    method visit_EForall :
+      'c -> Expr.t -> (string * Type.t option) list -> Expr.t -> Expr.t
+
     method visit_Emp : 'c -> Asrt.t -> Asrt.t
     method visit_Empty : 'c -> Literal.t -> Literal.t
     method visit_EmptyType : 'c -> Type.t -> Type.t
@@ -1872,6 +1878,7 @@ module Visitors : sig
          ; visit_EList : 'c -> Expr.t list -> 'f
          ; visit_ESet : 'c -> Expr.t list -> 'f
          ; visit_Exists : 'c -> (string * Type.t option) list -> Expr.t -> 'f
+         ; visit_EForall : 'c -> (string * Type.t option) list -> Expr.t -> 'f
          ; visit_Emp : 'c -> 'f
          ; visit_Empty : 'c -> 'f
          ; visit_EmptyType : 'c -> 'f
@@ -2104,6 +2111,7 @@ module Visitors : sig
     method visit_EList : 'c -> Expr.t list -> 'f
     method visit_ESet : 'c -> Expr.t list -> 'f
     method visit_Exists : 'c -> (string * Type.t option) list -> Expr.t -> 'f
+    method visit_EForall : 'c -> (string * Type.t option) list -> Expr.t -> 'f
     method visit_Emp : 'c -> 'f
     method visit_Empty : 'c -> 'f
     method visit_EmptyType : 'c -> 'f
@@ -2332,6 +2340,7 @@ module Visitors : sig
          ; visit_EList : 'c -> Expr.t list -> unit
          ; visit_ESet : 'c -> Expr.t list -> unit
          ; visit_Exists : 'c -> (string * Type.t option) list -> Expr.t -> unit
+         ; visit_EForall : 'c -> (string * Type.t option) list -> Expr.t -> unit
          ; visit_Emp : 'c -> unit
          ; visit_Empty : 'c -> unit
          ; visit_EmptyType : 'c -> unit
@@ -2565,6 +2574,7 @@ module Visitors : sig
     method visit_EList : 'c -> Expr.t list -> unit
     method visit_ESet : 'c -> Expr.t list -> unit
     method visit_Exists : 'c -> (string * Type.t option) list -> Expr.t -> unit
+    method visit_EForall : 'c -> (string * Type.t option) list -> Expr.t -> unit
     method visit_Emp : 'c -> unit
     method visit_Empty : 'c -> unit
     method visit_EmptyType : 'c -> unit

GillianCore/GIL_Syntax/TypeDef__.ml

@@ -141,6 +141,7 @@ and expr =
   | EList of expr list
   | ESet of expr list
   | Exists of (string * typ option) list * expr
+  | EForall of (string * typ option) list * expr
 
 and formula =
   | True

GillianCore/engine/Abstraction/MP.ml

@@ -148,7 +148,7 @@ let rec missing_expr (kb : KB.t) (e : Expr.t) : KB.t list =
               Fmt.(brackets (list ~sep:semi kb_pp))
               result);
         result
-    | Exists (bt, e) ->
+    | Exists (bt, e) | EForall (bt, e) ->
         let kb' =
           KB.add_seq (List.to_seq bt |> Seq.map (fun (x, _) -> Expr.LVar x)) kb
         in
@@ -286,7 +286,7 @@ let rec learn_expr
   (* TODO: Finish the remaining invertible binary operators *)
   | BinOp _ -> []
   (* Can we learn anything from Exists? *)
-  | Exists _ -> []
+  | Exists _ | EForall _ -> []
 
 and learn_expr_list (kb : KB.t) (le : (Expr.t * Expr.t) list) =
   (* L.(verbose (fun m -> m "Entering learn_expr_list: \nKB: %a\nList: %a" kb_pp kb Fmt.(brackets (list ~sep:semi (parens (pair ~sep:comma Expr.pp Expr.pp)))) le)); *)
@@ -325,7 +325,7 @@ let simple_ins_expr_collector =
           (KB.empty, KB.singleton e)
       | UnOp (LstLen, ((PVar s | LVar s) as v)) when not (SS.mem s exclude) ->
           (KB.singleton v, KB.empty)
-      | Exists (bt, e) ->
+      | Exists (bt, e) | EForall (bt, e) ->
           let exclude =
             List.fold_left (fun acc (x, _) -> SS.add x acc) exclude bt
           in

GillianCore/engine/Abstraction/Normaliser.ml

@@ -181,7 +181,7 @@ module Make (SPState : PState.S) = struct
                            "normalise_lexpr: program variable in normalised \
                             expression")
                   | BinOp (_, _, _) | UnOp (_, _) -> UnOp (TypeOf, nle1)
-                  | Exists _ -> Lit (Type BooleanType)
+                  | Exists _ | EForall _ -> Lit (Type BooleanType)
                   | EList _ | LstSub _ | NOp (LstCat, _) -> Lit (Type ListType)
                   | NOp (_, _) | ESet _ -> Lit (Type SetType))
               | _ -> UnOp (uop, nle1)))
@@ -231,6 +231,20 @@ module Make (SPState : PState.S) = struct
           match bt with
           | [] -> ne
           | _ -> Exists (bt, ne))
+      | EForall (bt, e) -> (
+          let new_gamma = Type_env.copy gamma in
+          List.iter
+            (fun (x, t) ->
+              match t with
+              | Some t -> Type_env.update new_gamma x t
+              | None -> Type_env.remove new_gamma x)
+            bt;
+          let ne = normalise_lexpr ~no_types ~store ~subst new_gamma e in
+          let lvars = Expr.lvars ne in
+          let bt = List.filter (fun (x, _) -> SS.mem x lvars) bt in
+          match bt with
+          | [] -> ne
+          | _ -> EForall (bt, ne))
     in
 
     if not no_types then Typing.infer_types_expr gamma result;

GillianCore/engine/FOLogic/Reduction.ml

@@ -135,6 +135,7 @@ let rec normalise_list_expressions (le : Expr.t) : Expr.t =
     | ESet lst -> ESet (List.map f lst)
     | LstSub (le1, le2, le3) -> LstSub (f le1, f le2, f le3)
     | Exists (bt, le) -> Exists (bt, f le)
+    | EForall (bt, le) -> EForall (bt, f le)
     (*
     | LstSub(le1, le2, le3) ->
       (match f le1, f le2, f le3 with
@@ -1678,8 +1679,25 @@ and reduce_lexpr_loop
             LstSub (fle1, fle2, fle3))
     (* CHECK: FTimes and Div are the same, how does the 'when' scope? *)
     | BinOp (lel, op, ler) -> (
-        let flel = f lel in
-        let fler = f ler in
+        let op_is_or_and () =
+          match op with
+          | BOr | BAnd -> true
+          | _ -> false
+        in
+        let flel, fler =
+          (* If we're reducing A || B or A && B and either side have a reduction exception, it must be false *)
+          let flel =
+            try f lel with
+            | ReductionException _ when op_is_or_and () -> Expr.bool false
+            | exn -> raise exn
+          in
+          let fler =
+            try f ler with
+            | ReductionException _ when op_is_or_and () -> Expr.bool false
+            | exn -> raise exn
+          in
+          (flel, fler)
+        in
         let def = Expr.BinOp (flel, op, fler) in
         match (flel, fler) with
         | Lit ll, Lit lr -> (
@@ -2000,6 +2018,43 @@ and reduce_lexpr_loop
         match bt with
         | [] -> re
         | _ -> Exists (bt, re))
+    | EForall (bt, e) -> (
+        (* We create a new pfs and gamma where:
+           - All shadowed variables are substituted with a fresh variable
+           - The gamma has been updated with the types given in the binder *)
+        let new_gamma = Type_env.copy gamma in
+        let new_pfs = PFS.copy pfs in
+        let subst_bindings = List.map (fun (x, _) -> (x, LVar.alloc ())) bt in
+        let subst =
+          SVal.SESubst.init
+            (List.map (fun (x, y) -> (Expr.LVar x, Expr.LVar y)) subst_bindings)
+        in
+        let () =
+          List.iter
+            (fun (x, t) ->
+              let () =
+                match Type_env.get new_gamma x with
+                | Some t ->
+                    let new_var = List.assoc x subst_bindings in
+                    Type_env.update new_gamma new_var t
+                | None -> ()
+              in
+              match t with
+              | Some t -> Type_env.update new_gamma x t
+              | None -> Type_env.remove new_gamma x)
+            bt
+        in
+        let () = PFS.substitution subst new_pfs in
+        (* We reduce using our new pfs and gamma *)
+        let re =
+          reduce_lexpr_loop ~matching ~reduce_lvars new_pfs new_gamma e
+        in
+        let vars = Expr.lvars re in
+        let bt = List.filter (fun (b, _) -> Containers.SS.mem b vars) bt in
+        (* We remove all quantifiers that aren't used anymore *)
+        match bt with
+        | [] -> re
+        | _ -> EForall (bt, re))
     (* The remaining cases cannot be reduced *)
     | _ -> le
   in

GillianCore/engine/FOLogic/typing.ml

@@ -177,6 +177,29 @@ module Infer_types_to_gamma = struct
               if not (List.exists (fun (y, _) -> String.equal x y) bt) then
                 Type_env.update new_gamma x t);
           ret
+    | EForall (bt, le) ->
+        if not (tt = BooleanType) then false
+        else
+          let gamma_copy = Type_env.copy gamma in
+          let new_gamma_copy = Type_env.copy new_gamma in
+          let () =
+            List.iter
+              (fun (x, t) ->
+                let () =
+                  match t with
+                  | Some t -> Type_env.update gamma_copy x t
+                  | None -> Type_env.remove gamma_copy x
+                in
+                Type_env.remove new_gamma_copy x)
+              bt
+          in
+          let ret = f' gamma_copy new_gamma_copy le BooleanType in
+          (* We've updated our new_gamma_copy with a bunch of things.
+             We need to import everything except the quantified variables to the new_gamma *)
+          Type_env.iter new_gamma_copy (fun x t ->
+              if not (List.exists (fun (y, _) -> String.equal x y) bt) then
+                Type_env.update new_gamma x t);
+          ret
 end
 
 let infer_types_to_gamma = Infer_types_to_gamma.f
@@ -439,7 +462,8 @@ module Type_lexpr = struct
       else def_neg
     else def_neg
 
-  and type_exists gamma le bt e =
+  (** Typing quantified expr is independant on the kind of quantifier *)
+  and type_quantified_expr gamma le bt e =
     let gamma_copy = Type_env.copy gamma in
     let () =
       List.iter
@@ -472,7 +496,7 @@ module Type_lexpr = struct
       | EList _ -> def_pos (Some ListType)
       (* Sets are always typable *)
       | ESet _ -> def_pos (Some SetType)
-      | Exists (bt, e) -> type_exists gamma le bt e
+      | Exists (bt, e) | EForall (bt, e) -> type_quantified_expr gamma le bt e
       | UnOp (op, e) -> type_unop gamma le op e
       | BinOp (e1, op, e2) -> type_binop gamma le op e1 e2
       | NOp (SetUnion, les) | NOp (SetInter, les) ->

GillianCore/engine/concrete_semantics/CExprEval.ml

@@ -552,7 +552,7 @@ and evaluate_expr (store : CStore.t) (e : Expr.t) : CVal.M.t =
     | NOp (nop, le) -> evaluate_nop nop (List.map ee le)
     | EList ll -> evaluate_elist store ll
     | LstSub (e1, e2, e3) -> evaluate_lstsub store e1 e2 e3
-    | ALoc _ | LVar _ | ESet _ | Exists _ ->
+    | ALoc _ | LVar _ | ESet _ | Exists _ | EForall _ ->
         raise
           (Exceptions.Impossible "eval_expr concrete: aloc, lvar, set or exists")
   with

GillianCore/engine/general_semantics/eSubst.ml

@@ -421,6 +421,20 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
         Seq.iter (fun (x, le_x) -> put self_subst (LVar x) le_x) binder_substs;
         if new_expr == e then this else Exists (bt, new_expr)
 
+      method! visit_EForall () this bt e =
+        let binders = List.to_seq bt |> Seq.map fst in
+        let binder_substs =
+          binders
+          |> Seq.filter_map (fun x ->
+                 Option.map (fun x_v -> (x, x_v)) (get self_subst (LVar x)))
+        in
+        Seq.iter
+          (fun x -> put self_subst (LVar x) (Val.from_lvar_name x))
+          binders;
+        let new_expr = self#visit_expr () e in
+        Seq.iter (fun (x, le_x) -> put self_subst (LVar x) le_x) binder_substs;
+        if new_expr == e then this else EForall (bt, new_expr)
+
       method! visit_ForAll () this bt form =
         let binders = List.to_seq bt |> Seq.map fst in
         let binders_substs =
@@ -475,6 +489,18 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
           List.iter (fun (x, _) -> Hashtbl.remove subst (Expr.LVar x)) bt;
           let result = Option.map (fun e' -> Expr.Exists (bt, e')) e' in
           (result, false)
+      | EForall (bt, e) ->
+          (* We use Hashtbl.add so that we can later remove the binding and recover the old one! *)
+          List.iter
+            (fun (x, _) ->
+              let lvar = Expr.LVar x in
+              let lvar_e = Option.get (Val.from_expr lvar) in
+              Hashtbl.add subst lvar lvar_e)
+            bt;
+          let e' = subst_in_expr_opt subst e in
+          List.iter (fun (x, _) -> Hashtbl.remove subst (Expr.LVar x)) bt;
+          let result = Option.map (fun e' -> Expr.EForall (bt, e')) e' in
+          (result, false)
       | _ -> (Some le, true)
     in
     Expr.map_opt f_before None le

GillianCore/engine/symbolic_semantics/SState.ml

@@ -259,6 +259,7 @@ module Make (SMemory : SMemory.S) :
         | LstSub (e1, e2, e3) -> LstSub (f e1, f e2, f e3)
         (* Exists. We can just evaluate pvars because they cannot be quantified *)
         | Exists (bt, e) -> Exists (bt, f e)
+        | EForall (bt, e) -> EForall (bt, f e)
         | Lit _ | LVar _ | ALoc _ -> expr
       in
       (* Perform reduction *)