Preds are just Core preds with ✨flavour✨

Gillian-C/lib/Constr.ml

@@ -42,8 +42,8 @@ module Others = struct
   (* The in/out split below must match the runtime predicate definitions, since
      the engine trusts the split carried by the assertion. All-ins predicates
      use [pred]; predicates with out-parameters spell out [ins] and [outs]. *)
-  let pred name ins outs = Asrt.Pred (name, ins, outs)
-  let pred_in name ins = Asrt.Pred (name, ins, [])
+  let pred name ins outs = Asrt.pred name ins outs
+  let pred_in name ins = Asrt.pred name ins []
 
   (* [i__malloced] is, unfortunately, declared with a different in/out split
      depending on the architecture: [(p; bytes)] in 64-bit, [(p, bytes;)] in

Gillian-C/lib/gil_logic_gen.ml

@@ -144,7 +144,7 @@ let assert_of_member cenv members id typ =
       let list_is_components = pvmember#==(Expr.list args_without_ins) in
       let ofs = Expr.Infix.(pvofs + fo) in
       (* Struct predicates have the location and offset as their two ins. *)
-      let pred_call = Asrt.Pred (pred_name, [ pvloc; ofs ], args_without_ins) in
+      let pred_call = Asrt.pred pred_name [ pvloc; ofs ] args_without_ins in
       [ list_is_components; pred_call ]
   | Tarray (ty, n, _) ->
       let n = ValueTranslation.int_of_z n in
@@ -166,13 +166,12 @@ let assert_of_member cenv members id typ =
         let open Internal_Predicates in
         let open VTypes in
         match typ with
-        | Tint _ ->
-            (mk int_type lvval, Asrt.Pred (int_get, [ pvmember ], [ lvval ]))
+        | Tint _ -> (mk int_type lvval, Asrt.pred int_get [ pvmember ] [ lvval ])
         | Tlong _ ->
-            (mk long_type lvval, Asrt.Pred (long_get, [ pvmember ], [ lvval ]))
+            (mk long_type lvval, Asrt.pred long_get [ pvmember ] [ lvval ])
         | Tfloat _ ->
-            (mk float_type lvval, Asrt.Pred (float_get, [ pvmember ], [ lvval ]))
-        | Tpointer _ -> (pvmember, Asrt.Pred (is_ptr_opt, [ pvmember ], []))
+            (mk float_type lvval, Asrt.pred float_get [ pvmember ] [ lvval ])
+        | Tpointer _ -> (pvmember, Asrt.pred is_ptr_opt [ pvmember ] [])
         | _ ->
             failwith
               (Printf.sprintf "unhandled struct field type for now : %s"
@@ -449,9 +448,7 @@ let trans_constr ?fname:_ ~(typ : CAssert.points_to_type) ann s c =
   let tloc = types ObjectType in
   (* let mk_num n = Expr.Lit (Num (float_of_int n)) in *)
   (* let zero = mk_num 0 in *)
-  let ptr_call p l o =
-    Asrt.Pred (Internal_Predicates.ptr_get, [ p ], [ l; o ])
-  in
+  let ptr_call p l o = Asrt.pred Internal_Predicates.ptr_get [ p ] [ l; o ] in
   let sz = function
     | CSVal.Sint _ -> 4
     | Slong _ -> 8
@@ -548,7 +545,7 @@ let trans_constr ?fname:_ ~(typ : CAssert.points_to_type) ann s c =
         split3_expr_comp (List.map trans_expr el)
       in
       let pr =
-        Asrt.Pred (struct_pred, [ locv; ofsv ], params_fields) :: more_asrt
+        Asrt.pred struct_pred [ locv; ofsv ] params_fields :: more_asrt
       in
       pr @ to_assert @ [ malloc_chunk siz ]
 
@@ -590,7 +587,7 @@ let rec trans_asrt ~fname ~ann asrt =
     | Pred (p, c_ins, c_outs) ->
         let ap_in, _, g_ins = split3_expr_comp (List.map trans_expr c_ins) in
         let ap_out, _, g_outs = split3_expr_comp (List.map trans_expr c_outs) in
-        Pred (p, g_ins, g_outs) :: (ap_in @ ap_out)
+        Asrt.pred p g_ins g_outs :: (ap_in @ ap_out)
     | Emp -> [ Asrt.Emp ]
     | PointsTo { ptr = s; constr = c; typ } -> trans_constr ~fname ~typ ann s c
   in
@@ -876,17 +873,17 @@ let bounds signedness bit_size =
   (Expr.int_z min, Expr.int_z max)
 
 let predicate_from_triple (e, csmt, ct) =
-  let pred pname = Asrt.Pred (pname, [ e ], []) in
+  let pred pname = Asrt.pred pname [ e ] [] in
   let open Internal_Predicates in
   match (csmt, ct) with
   | _, Ctypes.Tpointer (Tfunction _, _) -> pred is_ptr_to_0
   | _, Ctypes.Tpointer _ -> pred is_ptr_opt
   | AST.Tint, Tint (size, signedness, _) ->
       let min, max = bounds signedness (bit_size size) in
-      Asrt.Pred (Internal_Predicates.is_bounded_int, [ e; min; max ], [])
+      Asrt.pred Internal_Predicates.is_bounded_int [ e; min; max ] []
   | AST.Tlong, Tlong (signedness, _) ->
       let min, max = bounds signedness 64 in
-      Asrt.Pred (Internal_Predicates.is_bounded_long, [ e; min; max ], [])
+      Asrt.pred Internal_Predicates.is_bounded_long [ e; min; max ] []
   | AST.Tsingle, _ -> pred is_single
   | AST.Tfloat, _ -> pred is_float
   | _ ->

Gillian-C2/lib/compiler/constr.ml

@@ -36,8 +36,8 @@ module Others = struct
 
   (* The in/out split must match the runtime predicate definitions, since the
      engine trusts the split carried by the assertion. *)
-  let pred name ins outs = Asrt.Pred (name, ins, outs)
-  let pred_in name ins = Asrt.Pred (name, ins, [])
+  let pred name ins outs = Asrt.pred name ins outs
+  let pred_in name ins = Asrt.pred name ins []
 
   let malloced_abst ~ptr ~total_size =
     pred Internal_Predicates.malloced [ ptr ] [ total_size ]

Gillian-C2/lib/compiler/gil_logic_gen.ml

@@ -130,7 +130,7 @@ let convert_struct_field
         in
         let field_arg_list = pvmember#==(Expr.list field_args) in
         (* Struct predicates have the location and offset as their two ins. *)
-        let pred_call = Asrt.Pred (pred_name, [ pvloc; ofs ], field_args) in
+        let pred_call = Asrt.pred pred_name [ pvloc; ofs ] field_args in
         (Some GilType.ListType, [ field_arg_list; pred_call ])
     | Array (type_', len) ->
         let chunk =
@@ -165,14 +165,14 @@ let convert_struct_field
                     | I_ssize_t -> is_ssize_t
                     | I_bool -> is_bool
                   in
-                  let asrt = Asrt.Pred (pred, [ pvmember ], []) in
+                  let asrt = Asrt.pred pred [ pvmember ] [] in
                   Some (Some IntType, [ asrt ])
               | Signedbv _ | Unsignedbv _ | Enum _ | EnumTag _ ->
                   Some (Some IntType, [])
               | Double | Float -> Some (Some NumberType, [])
               | Pointer _ ->
                   let is_ptr_asrt =
-                    Asrt.Pred (Internal_Predicates.is_ptr, [ pvmember ], [])
+                    Asrt.pred Internal_Predicates.is_ptr [ pvmember ] []
                   in
                   Some (Some ListType, [ is_ptr_asrt ])
               | _ -> None
@@ -412,9 +412,7 @@ let trans_constr ~(ctx : Ctx.t) ~(typ : CAssert.points_to_type) ~pvar_map s c =
   let gen_ofs_var () = Expr.LVar (fresh_lvar ()) in
   let te = trans_expr ~pvar_map in
   let tse = trans_simpl_expr ~pvar_map in
-  let ptr_call p l o =
-    Asrt.Pred (Internal_Predicates.ptr_get, [ p ], [ l; o ])
-  in
+  let ptr_call p l o = Asrt.pred Internal_Predicates.ptr_get [ p ] [ l; o ] in
   let sz x = CSVal.size_of ~ctx x |> Z.of_int in
   let interpret_s ~typ s =
     match typ with
@@ -491,7 +489,7 @@ let trans_constr ~(ctx : Ctx.t) ~(typ : CAssert.points_to_type) ~pvar_map s c =
       in
       let more_asrt, _, params_fields = split3_expr_comp (List.map te el) in
       let pr =
-        Asrt.Pred (struct_pred, [ locv; ofsv ], params_fields) :: more_asrt
+        Asrt.pred struct_pred [ locv; ofsv ] params_fields :: more_asrt
       in
       pr @ to_assert @ [ malloc_chunk size ]
 
@@ -536,7 +534,7 @@ let rec trans_asrt ~ctx ~pvar_map asrt =
     | Pred (p, c_ins, c_outs) ->
         let ap_in, _, g_ins = split3_expr_comp (List.map te c_ins) in
         let ap_out, _, g_outs = split3_expr_comp (List.map te c_outs) in
-        Pred (p, g_ins, g_outs) :: (ap_in @ ap_out)
+        Asrt.pred p g_ins g_outs :: (ap_in @ ap_out)
     | Emp -> [ Asrt.Emp ]
     | PointsTo { ptr = s; constr = c; typ } ->
         trans_constr ~pvar_map ~ctx ~typ s c
@@ -684,7 +682,7 @@ let get_param_typasrt param =
     | _ -> None
   in
   match (pred, param.identifier) with
-  | Some pred, Some id -> Some (Asrt.Pred (pred, [ PVar id ], []))
+  | Some pred, Some id -> Some (Asrt.pred pred [ PVar id ] [])
   | _ -> None
 
 let trans_sspec ~ctx ~pvar_map ~params sspecs =
@@ -845,7 +843,7 @@ module Machine_preds = struct
       let perm = Expr.string Perm.(to_string Freeable) in
       Asrt.
         [
-          Pred (Internal_Predicates.ptr_get, [ PVar "p" ], [ l; Expr.zero_i ]);
+          Asrt.pred Internal_Predicates.ptr_get [ PVar "p" ] [ l; Expr.zero_i ];
           CorePred
             ( LActions.(str_ga Single),
               [ l; start; chunk ],

Gillian-C2/lib/memory_model/predicates.ml

@@ -37,8 +37,8 @@ module Others = struct
 
   (* The in/out split must match the runtime predicate definitions, since the
      engine trusts the split carried by the assertion. *)
-  let pred name ins outs = Asrt.Pred (name, ins, outs)
-  let pred_in name ins = Asrt.Pred (name, ins, [])
+  let pred name ins outs = Asrt.pred name ins outs
+  let pred_in name ins = Asrt.pred name ins []
 
   let malloced_abst ~ptr ~total_size =
     pred Internal_Predicates.malloced [ ptr ] [ total_size ]

Gillian-JS/lib/Compiler/JSIL2GIL.ml

@@ -83,7 +83,8 @@ let rec jsil2gil_asrt (a : Asrt.t) : GAsrt.t =
   | MetaData (e1, e2) -> [ Asrt_utils.metadata ~loc:(fe e1) ~metadata:(fe e2) ]
   | EmptyFields (e1, e2) ->
       [ Asrt_utils.empty_fields ~loc:(fe e1) ~domain:(fe e2) ]
-  | Pred (pn, ins, outs) -> [ Pred (pn, List.map fe ins, List.map fe outs) ]
+  | Pred (pn, ins, outs) ->
+      [ GAsrt.pred pn (List.map fe ins) (List.map fe outs) ]
   | Pure f -> [ Pure (jsil2gil_expr f) ]
   | Types vts -> [ Types (List.map (fun (v, t) -> (fe v, t)) vts) ]
 

Gillian-JS/lib/Compiler/JSIL_PostParser.ml

@@ -207,7 +207,7 @@ let scope_info_to_assertion
   let this_asrt = make_this_assertion () in
 
   if fid <> JS2JSIL_Helpers.main_fid then
-    let init_heap_asrt : Asrt.t = Pred (heap_asrt_name, [], []) in
+    let init_heap_asrt : Asrt.t = Asrt.Pred (heap_asrt_name, [], []) in
     Asrt.star
       (glob_constraints @ (this_asrt :: init_heap_asrt :: a_schain :: a_vars))
   else Asrt.star (glob_constraints @ (this_asrt :: a_schain :: a_vars))

GillianCore/GIL_Syntax/Asrt.ml

@@ -1,7 +1,6 @@
 (** {b GIL logic assertions}. *)
 type atom = TypeDef__.assertion_atom =
   | Emp  (** Empty heap *)
-  | Pred of string * Expr.t list * Expr.t list  (** Predicates *)
   | Pure of Expr.t  (** Pure formula *)
   | Types of (Expr.t * Type.t) list  (** Typing assertion *)
   | CorePred of string * Expr.t list * Expr.t list  (** Core assertion *)
@@ -16,6 +15,28 @@ let atom_of_yojson = TypeDef__.assertion_atom_of_yojson
 let to_yojson = TypeDef__.assertion_to_yojson
 let of_yojson = TypeDef__.assertion_of_yojson
 
+(* User-defined predicates no longer have their own assertion variant: they are
+   encoded as {!CorePred}s whose name is the user predicate name prefixed with
+   [user_pred_prefix]. The prefix is defined {b once}, here. *)
+let user_pred_prefix = "GILLIAN_USER_PRED__"
+
+(** [user_pred_name p] is the core-predicate name that encodes the user-defined
+    predicate [p]. *)
+let user_pred_name (name : string) : string = user_pred_prefix ^ name
+
+(** [as_user_pred_name s] returns [Some p] when the core-predicate name [s]
+    encodes a user-defined predicate [p] (i.e. [s = user_pred_name p]), and
+    [None] when [s] is a genuine core predicate. *)
+let as_user_pred_name (name : string) : string option =
+  let n = String.length user_pred_prefix in
+  if String.length name >= n && String.sub name 0 n = user_pred_prefix then
+    Some (String.sub name n (String.length name - n))
+  else None
+
+(** Builds a user-predicate assertion (a {!CorePred} with the encoded name). *)
+let pred (name : string) (ins : Expr.t list) (outs : Expr.t list) : atom =
+  CorePred (user_pred_name name, ins, outs)
+
 let compare x y =
   let cmp = Stdlib.compare in
   match (x, y) with
@@ -55,8 +76,8 @@ let prioritise (a1 : atom) (a2 : atom) =
   | Types [ (e, _) ], Types [ (e', _) ] -> lloc_aloc_pvar_lvar e e'
   | Types _, _ -> -1
   | _, Types _ -> 1
-  | Pred _, _ -> 1
-  | _, Pred _ -> -1
+  | CorePred (n1, _, _), _ when Option.is_some (as_user_pred_name n1) -> 1
+  | _, CorePred (n2, _, _) when Option.is_some (as_user_pred_name n2) -> -1
   | _, _ -> Stdlib.compare a1 a2
 
 module MyAssertion = struct
@@ -71,7 +92,6 @@ module Set = Set.Make (MyAssertion)
 let map (f_e : Expr.t -> Expr.t) : t -> t =
   List.map (function
     | Emp -> Emp
-    | Pred (s, ins, outs) -> Pred (s, List.map f_e ins, List.map f_e outs)
     | Pure form -> Pure (f_e form)
     | Types lt -> Types (List.map (fun (exp, typ) -> (f_e exp, typ)) lt)
     | CorePred (x, es1, es2) -> CorePred (x, List.map f_e es1, List.map f_e es2)
@@ -104,7 +124,11 @@ let pred_names : t -> string list =
     object
       inherit [_] Visitors.reduce
       inherit Visitors.Utils.non_ordered_list_monoid
-      method! visit_Pred () name _ _ = [ name ]
+
+      method! visit_CorePred () name _ _ =
+        match as_user_pred_name name with
+        | Some pred_name -> [ pred_name ]
+        | None -> []
     end
   in
   collector#visit_assertion ()
@@ -117,7 +141,7 @@ let pure_asrts : t -> Expr.t list =
 
 (* Check if --a-- is a pure assertion *)
 let is_pure_asrt : atom -> bool = function
-  | Pred _ | CorePred _ | Wand _ -> false
+  | CorePred _ | Wand _ -> false
   | _ -> true
 
 (* Eliminate Emp assertions.
@@ -135,17 +159,20 @@ let make_pure (a : t) : Expr.t =
 let _pp_atom ?(e_pp : Format.formatter -> Expr.t -> unit = Expr.pp) fmt =
   function
   | Emp -> Fmt.string fmt "emp"
-  | Pred (name, ins, outs) ->
-      let name = Pp_utils.maybe_quote_ident name in
-      let pp_e_l = Fmt.list ~sep:Fmt.comma e_pp in
-      Fmt.pf fmt "@[<h>%s(%a; %a)@]" name pp_e_l ins pp_e_l outs
   | Types tls ->
       let pp_tl f (e, t) = Fmt.pf f "%a : %s" e_pp e (Type.str t) in
       Fmt.pf fmt "types(@[%a@])" (Fmt.list ~sep:Fmt.comma pp_tl) tls
   | Pure f -> e_pp fmt f
-  | CorePred (a, ins, outs) ->
+  | CorePred (a, ins, outs) -> (
       let pp_e_l = Fmt.list ~sep:Fmt.comma e_pp in
-      Fmt.pf fmt "@[<h><%s>(%a; %a)@]" a pp_e_l ins pp_e_l outs
+      match as_user_pred_name a with
+      | Some pred_name ->
+          (* A user-defined predicate: printed [name(ins; outs)]. *)
+          let pred_name = Pp_utils.maybe_quote_ident pred_name in
+          Fmt.pf fmt "@[<h>%s(%a; %a)@]" pred_name pp_e_l ins pp_e_l outs
+      | None ->
+          (* A genuine core predicate: printed [<name>(ins; outs)]. *)
+          Fmt.pf fmt "@[<h><%s>(%a; %a)@]" a pp_e_l ins pp_e_l outs)
   | Wand { lhs = lname, largs; rhs = rname, rargs } ->
       let lname = Pp_utils.maybe_quote_ident lname in
       let rname = Pp_utils.maybe_quote_ident rname in

GillianCore/GIL_Syntax/Gil_syntax.mli

@@ -448,7 +448,6 @@ module Asrt : sig
 
   type atom =
     | Emp  (** Empty heap *)
-    | Pred of string * Expr.t list * Expr.t list  (** Predicates *)
     | Pure of Expr.t  (** Pure formula *)
     | Types of (Expr.t * Type.t) list  (** Typing assertion *)
     | CorePred of string * Expr.t list * Expr.t list  (** Core assertion *)
@@ -458,6 +457,21 @@ module Asrt : sig
 
   type t = atom list [@@deriving yojson, eq]
 
+  (** Prefix encoding a user-defined predicate as a {!CorePred} name. Set once;
+      never hardcode it elsewhere. *)
+  val user_pred_prefix : string
+
+  (** [user_pred_name p] is the core-predicate name encoding user predicate [p].
+  *)
+  val user_pred_name : string -> string
+
+  (** [as_user_pred_name s] is [Some p] when [s] encodes the user predicate [p],
+      and [None] when [s] is a genuine core predicate. *)
+  val as_user_pred_name : string -> string option
+
+  (** [pred name ins outs] builds a user-predicate assertion atom. *)
+  val pred : string -> Expr.t list -> Expr.t list -> atom
+
   (** Comparison of assertions *)
   val compare : atom -> atom -> int
 
@@ -1330,13 +1344,6 @@ module Visitors : sig
          ; visit_PhiAssignment :
              'c -> 'f Cmd.t -> (string * Expr.t list) list -> 'f Cmd.t
          ; visit_Pi : 'c -> Constant.t -> Constant.t
-         ; visit_Pred :
-             'c ->
-             Asrt.atom ->
-             string ->
-             Expr.t list ->
-             Expr.t list ->
-             Asrt.atom
          ; visit_Pure : 'c -> Asrt.atom -> Expr.t -> Asrt.atom
          ; visit_Random : 'c -> Constant.t -> Constant.t
          ; visit_ReturnError : 'c -> 'f Cmd.t -> 'f Cmd.t
@@ -1592,10 +1599,6 @@ module Visitors : sig
       'c -> 'f Cmd.t -> (string * Expr.t list) list -> 'f Cmd.t
 
     method visit_Pi : 'c -> Constant.t -> Constant.t
-
-    method visit_Pred :
-      'c -> Asrt.atom -> string -> Expr.t list -> Expr.t list -> Asrt.atom
-
     method visit_Pure : 'c -> Asrt.atom -> Expr.t -> Asrt.atom
     method visit_Random : 'c -> Constant.t -> Constant.t
     method visit_ReturnError : 'c -> 'f Cmd.t -> 'f Cmd.t
@@ -1851,7 +1854,6 @@ module Visitors : sig
          ; visit_Pi : 'c -> 'f
          ; visit_IPlus : 'c -> 'f
          ; visit_FPlus : 'c -> 'f
-         ; visit_Pred : 'c -> string -> Expr.t list -> Expr.t list -> 'f
          ; visit_Pure : 'c -> Expr.t -> 'f
          ; visit_Random : 'c -> 'f
          ; visit_ReturnError : 'c -> 'f
@@ -2069,7 +2071,6 @@ module Visitors : sig
     method visit_Pi : 'c -> 'f
     method visit_IPlus : 'c -> 'f
     method visit_FPlus : 'c -> 'f
-    method visit_Pred : 'c -> string -> Expr.t list -> Expr.t list -> 'f
     method visit_Pure : 'c -> Expr.t -> 'f
     method visit_Random : 'c -> 'f
     method visit_ReturnError : 'c -> 'f
@@ -2288,7 +2289,6 @@ module Visitors : sig
          ; visit_PVar : 'c -> string -> unit
          ; visit_PhiAssignment : 'c -> (string * Expr.t list) list -> unit
          ; visit_Pi : 'c -> unit
-         ; visit_Pred : 'c -> string -> Expr.t list -> Expr.t list -> unit
          ; visit_Pure : 'c -> Expr.t -> unit
          ; visit_Random : 'c -> unit
          ; visit_ReturnError : 'c -> unit
@@ -2507,7 +2507,6 @@ module Visitors : sig
     method visit_PVar : 'c -> string -> unit
     method visit_PhiAssignment : 'c -> (string * Expr.t list) list -> unit
     method visit_Pi : 'c -> unit
-    method visit_Pred : 'c -> string -> Expr.t list -> Expr.t list -> unit
     method visit_Pure : 'c -> Expr.t -> unit
     method visit_Random : 'c -> unit
     method visit_ReturnError : 'c -> unit