Remove Formula

Gillian-C/lib/Constr.ml

@@ -3,7 +3,7 @@ open Gil_syntax
 module Core = struct
   let pred ga ins outs =
     let ga_name = LActions.str_ga ga in
-    Asrt.GA (ga_name, ins, outs)
+    Asrt.CorePred (ga_name, ins, outs)
 
   let single ~loc ~ofs ~chunk ~sval ~perm =
     let chunk = Expr.Lit (String (ValueTranslation.string_of_chunk chunk)) in

Gillian-C/lib/MonadicSMemory.ml

@@ -24,7 +24,7 @@ let resolve_or_create_loc_name (lvar_loc : Expr.t) : string Delayed.t =
   match loc_name with
   | None ->
       let new_loc_name = ALoc.alloc () in
-      let learned = [ Formula.Eq (ALoc new_loc_name, lvar_loc) ] in
+      let learned = [ Expr.BinOp (ALoc new_loc_name, Equal, lvar_loc) ] in
       Logging.verbose (fun fmt ->
           fmt "Couldn't resolve loc %a, created %s" Expr.pp lvar_loc
             new_loc_name);
@@ -175,8 +175,8 @@ module Mem = struct
   let cons_array map loc ofs size chunk =
     let open DR.Syntax in
     let** loc_name = resolve_loc_result loc in
-    let open Formula.Infix in
-    if%sat size #<= (Expr.int 0) then
+    let open Expr.Infix in
+    if%sat size <= Expr.int 0 then
       DR.ok (map, MonadicSVal.SVArray.empty, Some Perm.Freeable)
     else
       let** tree = get_tree_res map loc_name (Some ofs) (Some chunk) in
@@ -187,8 +187,8 @@ module Mem = struct
 
   let prod_array map loc ofs size chunk array perm =
     let open DR.Syntax in
-    let open Formula.Infix in
-    if%sat size #<= (Expr.int 0) then DR.ok map
+    let open Expr.Infix in
+    if%sat size <= Expr.int 0 then DR.ok map
     else
       let* loc_name = resolve_or_create_loc_name loc in
       let* tree = get_or_create_tree map loc_name in
@@ -213,9 +213,9 @@ module Mem = struct
 
   let cons_simple ~sheap_consumer map loc low high =
     let open DR.Syntax in
-    let open Formula.Infix in
+    let open Expr.Infix in
     let** loc_name = resolve_loc_result loc in
-    if%sat high #<= low then DR.ok (map, Some Perm.Freeable)
+    if%sat high <= low then DR.ok (map, Some Perm.Freeable)
     else
       let** tree = get_tree_res map loc_name None None in
       let++ new_tree, perm =
@@ -225,8 +225,8 @@ module Mem = struct
 
   let prod_simple ~sheap_producer map loc low high perm =
     let open DR.Syntax in
-    let open Formula.Infix in
-    if%sat high #<= low then DR.ok map
+    let open Expr.Infix in
+    if%sat high <= low then DR.ok map
     else
       let* loc_name = resolve_or_create_loc_name loc in
       let* tree = get_or_create_tree map loc_name in
@@ -256,7 +256,7 @@ module Mem = struct
 
   let prod_bounds map loc bounds =
     let open DR.Syntax in
-    let** loc_name = resolve_loc_result loc in
+    let* loc_name = resolve_or_create_loc_name loc in
     let* tree = get_or_create_tree map loc_name in
     let++ tree_set =
       SHeapTree.prod_bounds tree bounds |> DR.of_result |> map_lift_err loc_name
@@ -265,8 +265,8 @@ module Mem = struct
 
   let move map dst_loc dst_ofs src_loc src_ofs sz =
     let open DR.Syntax in
-    let open Formula.Infix in
-    if%sat sz #== (Expr.int 0) then DR.ok map
+    let open Expr.Infix in
+    if%sat sz == Expr.int 0 then DR.ok map
     else
       let** dst_loc_name = resolve_loc_result dst_loc in
       let** src_loc_name = resolve_loc_result src_loc in
@@ -525,7 +525,7 @@ let execute_prod_single heap params =
   ] ->
       let perm = ValueTranslation.permission_of_string perm_string in
       let chunk = ValueTranslation.chunk_of_string chunk_string in
-      let* sval = SVal.of_gil_expr_exn sval_e in
+      let* sval = SVal.of_gil_expr_vanish sval_e in
       let++ mem = Mem.prod_single heap.mem loc ofs chunk sval perm in
       { heap with mem }
   | _ -> fail_ungracefully "set_single" params
@@ -955,7 +955,7 @@ let get_fixes err =
   | InvalidLocation loc ->
       let new_loc = ALoc.alloc () in
       let new_expr = Expr.ALoc new_loc in
-      [ [ Asrt.Pure (Eq (new_expr, loc)) ] ]
+      [ [ Asrt.Pure (BinOp (new_expr, Equal, loc)) ] ]
   | SHeapTreeErr
       {
         at_locations;

Gillian-C/lib/MonadicSVal.ml

@@ -8,38 +8,38 @@ module DR = Delayed_result
 exception NotACompCertValue of Expr.t
 
 module Patterns = struct
-  open Formula.Infix
+  open Expr.Infix
 
   let number e =
     let open Expr in
-    (typeof e) #== (type_ NumberType)
+    typeof e == type_ NumberType
 
   let integer e =
     let open Expr in
-    (typeof e) #== (type_ IntType)
+    typeof e == type_ IntType
 
   let int_typ, float_typ, single_typ, long_typ =
     let open Expr in
     let open CConstants.VTypes in
     let num_typ int_t typ_str x =
-      (typeof x) #== (type_ ListType)
-      #&& ((list_length x) #== (int 2))
-      #&& ((list_nth x 0) #== (string typ_str))
-      #&& ((typeof (list_nth x 1)) #== (type_ int_t))
+      typeof x == type_ ListType
+      && list_length x == int 2
+      && list_nth x 0 == string typ_str
+      && typeof (list_nth x 1) == type_ int_t
     in
     ( num_typ IntType int_type,
       num_typ NumberType float_type,
       num_typ NumberType single_type,
       num_typ IntType long_type )
 
-  let undefined x = x #== (Expr.Lit Undefined)
+  let undefined x = x == Expr.Lit Undefined
 
   let obj x =
     let open Expr in
-    (typeof x) #== (type_ ListType)
-    #&& ((list_length x) #== (int 2))
-    #&& ((typeof (list_nth x 0)) #== (type_ ObjectType))
-    #&& ((typeof (list_nth x 1)) #== (type_ IntType))
+    typeof x == type_ ListType
+    && list_length x == int 2
+    && typeof (list_nth x 0) == type_ ObjectType
+    && typeof (list_nth x 1) == type_ IntType
 end
 
 let of_chunk_and_expr chunk e =
@@ -72,11 +72,11 @@ let of_chunk_and_expr chunk e =
                     Expr.pp e))
       | Tlong -> return (SVlong e)
       | Tint ->
-          let open Formula.Infix in
+          let open Expr.Infix in
           let i k = Expr.int k in
           let learned =
             match chunk with
-            | Mint8unsigned -> [ (i 0) #<= e; e #<= (i 255) ]
+            | Mint8unsigned -> [ i 0 <= e; e <= i 255 ]
             | _ -> []
           in
           return ~learned (SVint e)
@@ -85,13 +85,13 @@ let of_chunk_and_expr chunk e =
       | Tany32 | Tany64 -> Fmt.failwith "Unhandled chunk: %a" Chunk.pp chunk)
 
 let of_gil_expr sval_e =
-  let open Formula.Infix in
+  let open Expr.Infix in
   let open Patterns in
   Logging.verbose (fun fmt -> fmt "OF_GIL_EXPR : %a" Expr.pp sval_e);
   let* sval_e = Delayed.reduce sval_e in
-  match%ent sval_e with
-  | undefined -> DO.some SUndefined
-  | obj ->
+  if%sat undefined sval_e then DO.some SUndefined
+  else
+    if%sat obj sval_e then
       let loc_expr = Expr.list_nth sval_e 0 in
       let ofs = Expr.list_nth sval_e 1 in
       let* ofs = Delayed.reduce ofs in
@@ -101,15 +101,20 @@ let of_gil_expr sval_e =
         | Some l -> (l, [])
         | None ->
             let aloc = ALoc.alloc () in
-            let learned = [ loc_expr #== (ALoc aloc) ] in
+            let learned = [ loc_expr == ALoc aloc ] in
             (aloc, learned)
       in
       DO.some ~learned (Sptr (loc, ofs))
-  | int_typ -> DO.some (SVint (Expr.list_nth sval_e 1))
-  | float_typ -> DO.some (SVfloat (Expr.list_nth sval_e 1))
-  | long_typ -> DO.some (SVlong (Expr.list_nth sval_e 1))
-  | single_typ -> DO.some (SVsingle (Expr.list_nth sval_e 1))
-  | _ -> DO.none ()
+    else
+      if%sat int_typ sval_e then DO.some (SVint (Expr.list_nth sval_e 1))
+      else
+        if%sat float_typ sval_e then DO.some (SVfloat (Expr.list_nth sval_e 1))
+        else
+          if%sat long_typ sval_e then DO.some (SVlong (Expr.list_nth sval_e 1))
+          else
+            if%sat single_typ sval_e then
+              DO.some (SVsingle (Expr.list_nth sval_e 1))
+            else DO.none ()
 
 let of_gil_expr_exn sval_e =
   let* value_opt = of_gil_expr sval_e in
@@ -119,6 +124,12 @@ let of_gil_expr_exn sval_e =
       if !Gillian.Utils.Config.under_approximation then Delayed.vanish ()
       else raise (NotACompCertValue sval_e)
 
+let of_gil_expr_vanish sval_e =
+  let* value_opt = of_gil_expr sval_e in
+  match value_opt with
+  | Some value -> Delayed.return value
+  | None -> Delayed.vanish ()
+
 let to_gil_expr_undelayed = to_gil_expr
 
 let to_gil_expr sval =
@@ -127,8 +138,8 @@ let to_gil_expr sval =
     List.map
       (fun (e, t) ->
         let open Expr in
-        let open Formula.Infix in
-        (typeof e) #== (type_ t))
+        let open Expr.Infix in
+        typeof e == type_ t)
       typings
   in
   Delayed.return ~learned:typing_pfs exp
@@ -163,10 +174,10 @@ module SVArray = struct
   let empty = Arr (EList [])
 
   let is_empty =
-    let open Formula.Infix in
+    let open Expr.Infix in
     function
-    | Arr e -> (Expr.list_length e) #== (Expr.int 0)
-    | _ -> False
+    | Arr e -> Expr.list_length e == Expr.int 0
+    | _ -> Expr.false_
 
   let sure_is_all_zeros = function
     | Arr (EList l) ->
@@ -194,8 +205,8 @@ module SVArray = struct
     in
     let learned =
       List.map
-        (let open Formula.Infix in
-         fun (e, t) -> (Expr.typeof e) #== (Expr.type_ t))
+        (let open Expr.Infix in
+         fun (e, t) -> Expr.typeof e == Expr.type_ t)
         gamma
     in
     (Expr.EList (List.rev rev_l), learned)
@@ -210,7 +221,7 @@ module SVArray = struct
       | None -> Expr.list_length arr_exp
       | Some size -> size
     in
-    let open Formula.Infix in
+    let open Expr.Infix in
     let zero = Expr.int 0 in
     let size = Engine.Reduction.reduce_lexpr size in
     match size with
@@ -220,24 +231,24 @@ module SVArray = struct
         let undefs =
           Expr.Lit (LList (List.init (Z.to_int x) (fun _ -> Literal.Undefined)))
         in
-        arr_exp #== undefs
+        arr_exp == undefs
     | _ ->
         Logging.verbose (fun fmt ->
             fmt "Undefined pf: not as concrete: %a" Expr.pp size);
         let i = LVar.alloc () in
         let i_e = Expr.LVar i in
         forall
           [ (i, Some IntType) ]
-          zero #<= i_e #&& (i_e #< size)
-          #=> ((Expr.list_nth_e arr_exp i_e) #== (Lit Undefined))
+          ((zero <= i_e && i_e < size)
+          ==> (Expr.list_nth_e arr_exp i_e == Lit Undefined))
 
   let zeros_pf ?size arr_exp =
     let size =
       match size with
       | None -> Expr.list_length arr_exp
       | Some size -> size
     in
-    let open Formula.Infix in
+    let open Expr.Infix in
     let size = Engine.Reduction.reduce_lexpr size in
     match size with
     | Lit (Int x) ->
@@ -246,26 +257,24 @@ module SVArray = struct
           Expr.Lit
             (LList (List.init (Z.to_int x) (fun _ -> Literal.Int Z.zero)))
         in
-        arr_exp #== zeros
+        arr_exp == zeros
     | _ ->
         Logging.verbose (fun fmt ->
             fmt "Zeros pf: not as concrete: %a" Expr.pp size);
-        let is_zero e = e #== (Expr.int 0) in
         let i = LVar.alloc () in
         let i_e = Expr.LVar i in
         let zero = Expr.int 0 in
         forall
           [ (i, Some IntType) ]
-          zero #<= i_e #&& (i_e #< size)
-          #=> (is_zero (Expr.list_nth_e arr_exp i_e))
+          ((zero <= i_e && i_e < size) ==> (Expr.list_nth_e arr_exp i_e == zero))
 
   let to_arr_with_size arr s =
-    let open Formula.Infix in
-    let allocate_array_lvar (descr : ?size:Expr.t -> Expr.t -> Formula.t) =
+    let open Expr.Infix in
+    let allocate_array_lvar (descr : ?size:Expr.t -> Expr.t -> Expr.t) =
       let x = LVar.alloc () in
       let learned_types = [ (x, Gil_syntax.Type.ListType) ] in
       let x = Expr.LVar x in
-      let learned = [ (Expr.list_length x) #== s; descr ~size:s x ] in
+      let learned = [ Expr.list_length x == s; descr ~size:s x ] in
       Delayed.return ~learned ~learned_types x
     in
     match arr with
@@ -332,27 +341,24 @@ module SVArray = struct
       | Lit (Int n) ->
           (Expr.EList (Utils.List_utils.make (Z.to_int n) concrete_single), [])
       | _ ->
-          let open Formula.Infix in
+          let open Expr.Infix in
           let arr = LVar.alloc () in
           let arr_e = Expr.LVar arr in
           let learned =
             let open Expr in
             [
-              (typeof arr_e) #== (type_ ListType);
-              (list_length arr_e) #== size;
+              typeof arr_e == type_ ListType;
+              list_length arr_e == size;
               describing_pf arr_e;
             ]
           in
           (arr_e, learned)
     in
     match svarr with
     | Arr e ->
-        let open Formula.Infix in
+        let open Expr.Infix in
         let learned =
-          [
-            (Expr.typeof e) #== (Expr.type_ ListType);
-            (Expr.list_length e) #== size;
-          ]
+          [ Expr.typeof e == Expr.type_ ListType; Expr.list_length e == size ]
         in
         (e, learned)
     | AllZeros ->
@@ -387,8 +393,8 @@ module SVArray = struct
                 (function
                   | Expr.Lit Undefined -> []
                   | x ->
-                      let open Formula.Infix in
-                      [ (i low) #<= x; x #<= (i high) ])
+                      let open Expr.Infix in
+                      [ i low <= x; x <= i high ])
                 e
             in
             Delayed.return ~learned ()
@@ -400,8 +406,8 @@ module SVArray = struct
                   List.concat
                     (List.init (Z.to_int n) (fun k ->
                          let x = Expr.list_nth e k in
-                         let open Formula.Infix in
-                         [ (i low) #<= x; x #<= (i high) ]))
+                         let open Expr.Infix in
+                         [ i low <= x; x <= i high ]))
                 in
                 Delayed.return ~learned ()
             | _ -> Delayed.return ())