[Logic] New predicate object_pointer. Not yet supported by the plugins.

src/kernel_internals/parsing/logic_lexer.mll

@@ -232,6 +232,7 @@
         "\\typeof", TYPEOF;
         "\\unallocated", UNALLOCATED;
         "\\union", BSUNION;
+        "\\object_pointer", OBJECT_POINTER;
         "\\valid", VALID;
         "\\valid_read", VALID_READ;
         "\\valid_index", VALID_INDEX;

src/kernel_internals/parsing/logic_parser.mly

@@ -243,7 +243,8 @@
 %token INT INTEGER REAL BOOLEAN BOOL FLOAT LT GT LE GE EQ NE COMMA ARROW EQUAL
 %token FORALL EXISTS IFF IMPLIES AND OR NOT SEPARATED
 %token TRUE FALSE OLD AT RESULT
-%token BLOCK_LENGTH BASE_ADDR OFFSET VALID VALID_READ VALID_INDEX VALID_RANGE VALID_FUNCTION
+%token BLOCK_LENGTH BASE_ADDR OFFSET VALID VALID_READ VALID_INDEX VALID_RANGE
+%token OBJECT_POINTER VALID_FUNCTION
 %token ALLOCATION STATIC REGISTER AUTOMATIC DYNAMIC UNALLOCATED
 %token ALLOCABLE FREEABLE FRESH
 %token DOLLAR QUESTION MINUS PLUS STAR AMP SLASH PERCENT LSQUARE RSQUARE EOF
@@ -456,6 +457,7 @@ lexpr_inner:
 | NOT lexpr_inner { info (PLnot $2) }
 | TRUE { info PLtrue }
 | FALSE { info PLfalse }
+| OBJECT_POINTER opt_label_1 LPAR lexpr RPAR { info (PLobject_pointer ($2,$4)) }
 | VALID opt_label_1 LPAR lexpr RPAR { info (PLvalid ($2,$4)) }
 | VALID_READ opt_label_1 LPAR lexpr RPAR { info (PLvalid_read ($2,$4)) }
 | VALID_FUNCTION LPAR lexpr RPAR { info (PLvalid_function $3) }
@@ -1932,6 +1934,7 @@ bs_keyword:
 | TYPEOF { () }
 | BSUNION { () }
 | UNALLOCATED { () }
+| OBJECT_POINTER { () }
 | VALID { () }
 | VALID_INDEX { () }
 | VALID_RANGE { () }

src/kernel_services/analysis/logic_interp.ml

@@ -800,7 +800,7 @@ to function contracts."
              taken into account by the functions [from_...] below *)
           DoChildren
 
-      | Pvalid_function _ ->
+      | Pobject_pointer _ | Pvalid_function _ ->
           DoChildren
 
       | Papp _ | Pallocable _ | Pfreeable _ | Pfresh _

src/kernel_services/ast_data/cil_types.mli

@@ -1569,6 +1569,8 @@ and predicate_node =
   | Pexists of quantifiers * predicate (** existential quantification. *)
   | Pat of predicate * logic_label
   (** predicate refers to a particular program point. *)
+  | Pobject_pointer of logic_label * term
+  (** the given locations can be pointed to. *)
   | Pvalid_read of logic_label * term   (** the given locations are valid for reading. *)
   | Pvalid of logic_label * term   (** the given locations are valid. *)
   | Pvalid_function of term

src/kernel_services/ast_printing/cil_printer.ml

@@ -231,6 +231,7 @@ module Precedence = struct
     | Pfreeable _
     | Pvalid _
     | Pvalid_read _
+    | Pobject_pointer _
     | Pvalid_function _
     | Pinitialized _
     | Pdangling _
@@ -2727,6 +2728,10 @@ class cil_printer () = object (self)
       fprintf fmt "@[%a%a(@[%a@])@]"
         self#pp_acsl_keyword "\\valid_read"
         self#labels [l] self#term p
+    | Pobject_pointer (l,p) ->
+      fprintf fmt "@[%a%a(@[%a@])@]"
+        self#pp_acsl_keyword "\\object_pointer"
+        self#labels [l] self#term p
     | Pvalid_function p ->
       fprintf fmt "@[%a(@[%a@])@]"
         self#pp_acsl_keyword "\\valid_function"

src/kernel_services/ast_printing/cil_types_debug.ml

@@ -859,6 +859,8 @@ and pp_predicate_node fmt = function
     Format.fprintf fmt "Pexists(%a,%a)"  pp_quantifiers quantifiers  pp_predicate predicate
   | Pat(predicate,logic_label) ->
     Format.fprintf fmt "Pat(%a,%a)"  pp_predicate predicate  pp_logic_label logic_label
+  | Pobject_pointer(logic_label,term) ->
+    Format.fprintf fmt "Pobject_pointer(%a,%a)"  pp_logic_label logic_label  pp_term term
   | Pvalid_read(logic_label,term) ->
     Format.fprintf fmt "Pvalid_read(%a,%a)"  pp_logic_label logic_label  pp_term term
   | Pvalid(logic_label,term) ->

src/kernel_services/ast_printing/logic_print.ml

@@ -129,7 +129,7 @@ let getParenthLevel e =
   | PLapp _ | PLold _ | PLat _
   | PLoffset _ | PLbase_addr _ | PLblock_length _
   | PLupdate _  | PLinitField _ | PLinitIndex _
-  | PLvalid _ | PLvalid_read _ | PLvalid_function _
+  | PLvalid _ | PLvalid_read _ | PLobject_pointer _ | PLvalid_function _
   | PLinitialized _ | PLdangling _
   | PLallocable _ | PLfreeable _ | PLfresh _
   | PLseparated _ | PLunion _ | PLinter _ -> 10
@@ -249,8 +249,12 @@ and print_lexpr_level n fmt e =
     | PLexists(q,e) ->
       fprintf fmt "@[\\exists@ @[%a@];@ %a@]"
         print_quantifiers q print_lexpr e
-    | PLvalid (l,e) -> fprintf fmt "\\valid%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
-    | PLvalid_read (l,e) -> fprintf fmt "\\valid_read%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+    | PLvalid (l,e) ->
+      fprintf fmt "\\valid%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+    | PLvalid_read (l,e) ->
+      fprintf fmt "\\valid_read%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+    | PLobject_pointer (l,e) ->
+      fprintf fmt "\\object_pointer%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
     | PLvalid_function e ->
       fprintf fmt "\\valid_function(@;@[%a@]@;)" print_lexpr_plain e
     | PLinitialized (l,e) ->

src/kernel_services/ast_queries/cil.ml

@@ -1868,6 +1868,10 @@ and childrenPredicateNode vis p =
     let s' = visitCilLogicLabel vis s in
     let t' = vTerm t in
     if t' != t || s != s' then Pvalid_read (s',t') else p
+  | Pobject_pointer (s,t) ->
+    let s' = visitCilLogicLabel vis s in
+    let t' = vTerm t in
+    if t' != t || s != s' then Pobject_pointer (s',t') else p
   | Pvalid_function t ->
     let t' = vTerm t in
     if t' != t then Pvalid_function t' else p
@@ -6945,7 +6949,7 @@ and free_vars_predicate bound_vars p = match p.pred_content with
          Logic_var.Set.union (free_vars_term bound_vars t) acc)
       Logic_var.Set.empty tl
   | Pallocable (_,t) | Pfreeable (_,t)
-  | Pvalid (_,t) | Pvalid_read (_,t) | Pvalid_function t
+  | Pvalid (_,t) | Pvalid_read (_,t) | Pobject_pointer (_, t) | Pvalid_function t
   | Pinitialized (_,t) | Pdangling (_,t) ->
     free_vars_term bound_vars t
   | Pseparated seps ->

src/kernel_services/ast_queries/logic_const.ml

@@ -425,6 +425,7 @@ let pallocable ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Palloca
 let pfreeable ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Pfreeable (l,p))
 let pvalid ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Pvalid (l,p))
 let pvalid_read ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Pvalid_read (l,p))
+let pobject_pointer ?(loc=Cil_datatype.Location.unknown) (l,p) = unamed ~loc (Pobject_pointer (l,p))
 let pvalid_function ?(loc=Cil_datatype.Location.unknown) p = unamed ~loc (Pvalid_function p)
 
 (* the index should be an integer or a range of integers *)

src/kernel_services/ast_queries/logic_const.mli

@@ -170,6 +170,9 @@ val pvalid_read: ?loc:location -> logic_label * term -> predicate
 (** \valid *)
 val pvalid: ?loc:location -> logic_label * term -> predicate
 
+(** \object_pointer *)
+val pobject_pointer: ?loc:location -> logic_label * term -> predicate
+
 (** \valid_function *)
 val pvalid_function: ?loc:location -> term -> predicate
 

src/kernel_services/ast_queries/logic_typing.ml

@@ -1049,7 +1049,8 @@ struct
       | Pimplies(p1,p2) | Piff(p1,p2) -> needs_at_pred p1 || needs_at_pred p2
       | Pnot p | Plet (_,p) | Pforall(_,p) | Pexists(_,p) -> needs_at_pred p
       | Pif(t,p1,p2) -> needs_at t || needs_at_pred p1 || needs_at_pred p2
-      | Pvalid (_,t) | Pvalid_read (_,t) | Pvalid_function t
+      | Pvalid (_,t) | Pvalid_read (_,t)
+      | Pobject_pointer (_,t) | Pvalid_function t
       | Pinitialized (_,t) | Pdangling (_, t)
       | Pallocable(_,t) | Pfreeable(_,t)-> needs_at t
       | Pfresh (_,_,t,n) -> (needs_at t) && (needs_at n)
@@ -3003,7 +3004,7 @@ struct
       let t2,ty2 = type_num_term_option ctxt env t2 in
       (Trange(t1,t2),
        Ltype(ctxt.find_logic_type "set", [arithmetic_conversion ty1 ty2]))
-    | PLvalid _ | PLvalid_read _ | PLvalid_function _
+    | PLvalid _ | PLvalid_read _ | PLobject_pointer _ | PLvalid_function _
     | PLfresh _ | PLallocable _ | PLfreeable _
     | PLinitialized _ | PLdangling _ | PLexists _ | PLforall _
     | PLimplies _ | PLiff _
@@ -3357,6 +3358,8 @@ struct
       predicate_label_ptr ~check_non_void:true pvalid_read l t
     | PLvalid (l,t) ->
       predicate_label_ptr ~check_non_void:true pvalid l t
+    | PLobject_pointer (l,t) ->
+      predicate_label_ptr ~check_non_void:false pobject_pointer l t
     | PLvalid_function t ->
       let t = term env t in
       if isLogicPointer t then begin

src/kernel_services/ast_queries/logic_utils.ml

@@ -935,6 +935,7 @@ and is_same_predicate_node p1 p2 =
   | Pfreeable (l1,t1), Pfreeable (l2,t2)
   | Pvalid (l1,t1), Pvalid (l2,t2)
   | Pvalid_read (l1,t1), Pvalid_read (l2,t2)
+  | Pobject_pointer (l1,t1), Pobject_pointer (l2,t2)
   | Pinitialized (l1,t1), Pinitialized (l2,t2) ->
     is_same_logic_label l1 l2 && is_same_term t1 t2
   | Pvalid_function t1, Pvalid_function t2 ->
@@ -949,7 +950,7 @@ and is_same_predicate_node p1 p2 =
      with Invalid_argument _ -> false)
   | (Pfalse | Ptrue | Papp _ | Prel _ | Pand _ | Por _ | Pimplies _
     | Piff _ | Pnot _ | Pif _ | Plet _ | Pforall _ | Pexists _
-    | Pat _ | Pvalid _ | Pvalid_read _ | Pvalid_function _
+    | Pat _ | Pvalid _ | Pvalid_read _ | Pobject_pointer _ | Pvalid_function _
     | Pinitialized _ | Pdangling _
     | Pfresh _ | Pallocable _ | Pfreeable _ | Pxor _ | Pseparated _
     ), _ -> false
@@ -1288,6 +1289,7 @@ and is_same_lexpr l1 l2 =
   | PLfreeable (l1,e1), PLfreeable (l2,e2)
   | PLvalid (l1,e1), PLvalid (l2,e2)
   | PLvalid_read (l1,e1), PLvalid_read (l2,e2)
+  | PLobject_pointer (l1,e1), PLobject_pointer (l2,e2)
   | PLbase_addr (l1,e1), PLbase_addr (l2,e2)
   | PLoffset (l1,e1), PLoffset (l2,e2)
   | PLblock_length (l1,e1), PLblock_length (l2,e2)
@@ -1316,7 +1318,8 @@ and is_same_lexpr l1 l2 =
     | PLupdate _ | PLinitIndex _ | PLtype _ | PLfalse
     | PLtrue | PLinitField _ | PLrel _ | PLand _ | PLor _ | PLxor _
     | PLimplies _ | PLiff _ | PLnot _ | PLif _ | PLforall _
-    | PLexists _ | PLvalid _ | PLvalid_read _ | PLvalid_function _
+    | PLexists _ | PLvalid _ | PLvalid_read _
+    | PLobject_pointer _ | PLvalid_function _
     | PLfreeable _ | PLallocable _
     | PLinitialized _ | PLdangling _ | PLseparated _ | PLfresh _ | PLnamed _
     | PLcomprehension _ | PLunion _ | PLinter _
@@ -1523,6 +1526,8 @@ and hash_predicate (acc,depth,tot) p =
       hash_predicate (acc + 173 + hash_label l, depth - 1, tot - 1) p
     | Pvalid_read (l, t) ->
       hash_term (acc + 187 + hash_label l, depth - 1, tot - 1) t
+    | Pobject_pointer (l, t) ->
+      hash_term (acc + 181 + hash_label l, depth - 1, tot - 1) t
     | Pvalid (l, t) ->
       hash_term (acc + 193 + hash_label l, depth - 1, tot - 1) t
     | Pvalid_function t -> hash_term (acc + 203, depth - 1, tot - 1) t
@@ -1823,6 +1828,7 @@ and compare_predicate_node p1 p2 =
   | Pfreeable (l1,t1), Pfreeable (l2,t2)
   | Pvalid (l1,t1), Pvalid (l2,t2)
   | Pvalid_read (l1,t1), Pvalid_read (l2,t2)
+  | Pobject_pointer (l1,t1), Pobject_pointer (l2,t2)
   | Pinitialized (l1,t1), Pinitialized (l2,t2)
   | Pdangling (l1,t1), Pdangling (l2,t2) ->
     let res = compare_logic_label l1 l2 in
@@ -1835,6 +1841,8 @@ and compare_predicate_node p1 p2 =
   | _, Pvalid _ -> -1
   | Pvalid_read _, _ -> 1
   | _, Pvalid_read _ -> -1
+  | Pobject_pointer _, _ -> 1
+  | _, Pobject_pointer _ -> -1
   | Pinitialized _, _ -> 1
   | _, Pinitialized _ -> -1
   | Pdangling _, _ -> 1

src/kernel_services/parsetree/logic_ptree.mli

@@ -132,6 +132,7 @@ and lexpr_node =
                                 expression. *)
   | PLvalid of string option * lexpr (** pointer is valid. *)
   | PLvalid_read of string option * lexpr (** pointer is valid for reading. *)
+  | PLobject_pointer of string option * lexpr (** object pointer can be created. *)
   | PLvalid_function of lexpr (** function pointer is compatible with pointed type. *)
   | PLallocable of string option * lexpr (** pointer is valid for malloc. *)
   | PLfreeable of string option * lexpr (** pointer is valid for free. *)

src/plugins/e-acsl/src/analyses/mmodel_analysis.ml

@@ -359,7 +359,8 @@ module rec Transfer
   let register_object kf state_ref = object
     inherit Visitor.frama_c_inplace
     method !vpredicate_node = function
-    | Pvalid(_, t) | Pvalid_read(_, t) | Pvalid_function t
+    | Pvalid(_, t) | Pvalid_read(_, t)
+    | Pobject_pointer(_, t) | Pvalid_function t
     | Pinitialized(_, t) | Pfreeable(_, t) ->
       (*	Options.feedback "REGISTER %a" Cil.d_term t;*)
       state_ref := register_term kf !state_ref t;

src/plugins/e-acsl/src/analyses/typing.ml

@@ -676,6 +676,7 @@ let rec type_predicate p =
     | Pallocable(_, t)
     | Pvalid(_, t)
     | Pvalid_read(_, t)
+    | Pobject_pointer(_,t)
     | Pvalid_function t ->
       ignore (type_term ~use_gmp_opt:false ~ctx:Nan t);
       c_int

src/plugins/e-acsl/src/code_generator/translate.ml

@@ -708,6 +708,7 @@ and named_predicate_content_to_exp ?name kf env p =
     e, env
   | Pseparated _ -> not_yet env "\\separated"
   | Pdangling _ -> not_yet env "\\dangling"
+  | Pobject_pointer _ -> not_yet env "\\object_pointer"
   | Pvalid_function _ -> not_yet env "\\valid_function"
   | Prel(rel, t1, t2) ->
     let ity = Typing.get_integer_op_of_predicate p in

src/plugins/value/legacy/eval_terms.ml

@@ -2144,6 +2144,7 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
     | _,Pvalid_read (_label,tsets) ->
       reduce_by_valid env positive Read tsets
 
+    | _,Pobject_pointer (_label, _tsets) -> env (* TODO *)
     | _,Pvalid_function _tsets -> env (* TODO *)
 
     | _,(Pinitialized (lbl_initialized,tsets)
@@ -2291,6 +2292,8 @@ and eval_predicate env pred =
       ignore (env_state env lbl);
       do_eval { env with e_cur = lbl } p
 
+    | Pobject_pointer (_label, _tsets) -> Unknown (* TODO *)
+
     | Pvalid (_label, tsets) | Pvalid_read (_label, tsets) ->
       (* TODO: see same constructor in reduce_by_predicate *)
       let kind = match p.pred_content with Pvalid_read _ -> Read | _ -> Write in
@@ -2579,7 +2582,8 @@ let predicate_deps env pred =
     | Pat (p, lbl) ->
       do_eval { env with e_cur = lbl } p
 
-    | Pvalid (_, tsets) | Pvalid_read (_, tsets) | Pvalid_function tsets->
+    | Pvalid (_, tsets) | Pvalid_read (_, tsets)
+    | Pobject_pointer (_, tsets) | Pvalid_function tsets ->
       (eval_term_as_lval ~alarm_mode env tsets).ldeps
 
     | Pinitialized (lbl, tsets) | Pdangling (lbl, tsets) ->

src/plugins/wp/LogicSemantics.ml

@@ -872,6 +872,11 @@ struct
     | Pvalid(label,t) -> valid env RW label t
     | Pvalid_read(label,t) -> valid env RD label t
 
+    | Pobject_pointer(_label,_t) ->
+        Warning.error
+          "\\object_pointer not yet implemented@\n\
+           @[<hov 0>(%a)@]" Printer.pp_predicate p
+
     | Pvalid_function _t ->
         Warning.error
           "\\valid_function not yet implemented@\n\

src/plugins/wp/RefUsage.ml

@@ -535,7 +535,8 @@ and pred (env:ctx) p : value = match p.pred_content with
   (* No escape *)
   | Pinitialized(_, t) | Pdangling(_,t)
   | Pallocable(_, t) | Pfreeable(_, t)
-  | Pvalid(_,t) | Pvalid_read (_,t) | Pvalid_function t ->
+  | Pvalid(_,t) | Pvalid_read (_,t)
+  | Pobject_pointer (_,t) | Pvalid_function t ->
       unescape ((term env) t)
   | Pseparated ts ->
       E.fcup (fun t -> unescape ((term env) t)) ts

src/plugins/wp/RegionAccess.ml

@@ -369,7 +369,7 @@ and cc_pred (map:map) (p:predicate) =
   | Pforall(_,p) | Pexists(_,p) -> cc_pred map p
 
   | Pseparated ts -> List.iter (cc_term map) ts
-  | Pvalid(_,t) | Pvalid_read(_,t) | Pvalid_function t
+  | Pvalid(_,t) | Pvalid_read(_,t) | Pobject_pointer(_,t) | Pvalid_function t
   | Pinitialized(_,t) | Pdangling(_,t) | Pallocable(_,t)
   | Pfreeable(_,t) -> cc_term map t
   | Pfresh(_,_,ptr,n) -> cc_term map ptr ; cc_term map n