CN VIP: Warn on using == for pointers

The definition of == in PNVI-ae-udi is complicated, but the spec language requires it to be simply mathematical equality on the tuple components. This commit warns when a user uses "==" so that it can be replace with new definitions, such as "is_null" or "ptr_eq".
rems-project · Nov 8, 2023 · af5abdb · af5abdb
1 parent d385164
commit af5abdb
Show file tree

Hide file tree

Showing 16 changed files with 51 additions and 20 deletions.
diff --git a/backend/cn/builtins.ml b/backend/cn/builtins.ml
@@ -51,7 +51,7 @@ let not_def = ("not", Sym.fresh_named "not", mk_arg1 not_)
 
 let nth_list_def = ("nth_list", Sym.fresh_named "nth_list", mk_arg3 nthList_)
 
-let array_to_list_def = 
+let array_to_list_def =
   ("array_to_list", Sym.fresh_named "array_to_list", mk_arg3_err
   (fun loc (arr, i, len) -> match SBT.is_map_bt (IT.bt arr) with
     | None -> fail {loc; msg = Illtyped_it {it = IT.pp arr; has = SBT.pp (IT.bt arr); expected = "map"; o_ctxt = None}}
@@ -65,7 +65,7 @@ let in_loc_list_def =
 
 let cellpointer_def =
   ("cellPointer",
-   Sym.fresh_named "cellPointer", 
+   Sym.fresh_named "cellPointer",
    mk_arg5 (fun (base, step, starti, endi, p) ->
        let base = IT.term_of_sterm base in
        let step = IT.term_of_sterm step in
@@ -76,12 +76,29 @@ let cellpointer_def =
      )
   )
 
-let builtin_funs = 
+let is_null_def =
+  ("is_null",
+   Sym.fresh_named "is_null",
+   mk_arg1 (fun p ->
+       IT.sterm_of_term IT.(eq_ (IT.term_of_sterm p, null_))
+     )
+  )
+
+let ptr_eq_def =
+    ("ptr_eq",
+        Sym.fresh_named "ptr_eq",
+        mk_arg2 (fun (p1, p2) ->
+       IT.sterm_of_term IT.(eq_ (IT.term_of_sterm p1, IT.term_of_sterm p2))
+     )
+   )
+
+
+let builtin_funs =
   [
       mul_uf_def;
       div_uf_def;
       power_uf_def;
-      rem_uf_def;  
+      rem_uf_def;
       mod_uf_def;
       xor_uf_def;
       bw_and_uf_def;
@@ -102,6 +119,8 @@ let builtin_funs =
       in_loc_list_def;
 
       cellpointer_def;
+      is_null_def;
+      ptr_eq_def;
     ]
 
 let apply_builtin_funs loc fsym args =

diff --git a/backend/cn/compile.ml b/backend/cn/compile.ml
@@ -508,8 +508,16 @@ module EffectfulTranslation = struct
     | CN_div, _ ->
         return (IT (Binop (Div, e1, e2), IT.bt e1))
     | CN_equal, _ ->
+      (match IT.bt e1, IT.bt e2 with
+       | Loc _, Loc _ ->
+         Pp.warn loc !^"pointer equality check"
+       | _, _ -> ());
         return (IT (Binop (EQ, e1, e2), SBT.Bool))
     | CN_inequal, _ ->
+      (match IT.bt e1, IT.bt e2 with
+       | Loc _, Loc _ ->
+         Pp.warn loc !^"pointer inequality check"
+       | _, _ -> ());
         return (not_ (IT (Binop (EQ, e1, e2), SBT.Bool)))
     | CN_lt, (SBT.Integer | SBT.Real) ->
         return (IT (Binop (LT, e1, e2), SBT.Bool))
@@ -800,7 +808,9 @@ module EffectfulTranslation = struct
         | CNExpr_unchanged e ->
            let@ cur_e = self e in
            let@ old_e = self (CNExpr (loc, CNExpr_at_env (e, start_evaluation_scope))) in
-           mk_translate_binop loc CN_equal (cur_e, old_e)
+           (* want to bypass the warning for (Loc, Loc) equality *)
+           (* mk_translate_binop loc CN_equal (cur_e, old_e) *)
+           return (IT (Binop (EQ, cur_e, old_e), SBT.Bool))
         | CNExpr_at_env (e, scope) ->
            let@ () = match evaluation_scope with
              | None -> return ()

diff --git a/backend/cn/solver.ml b/backend/cn/solver.ml
@@ -592,9 +592,11 @@ module Translate = struct
          | SetDifference -> Z3.Set.mk_difference context (term t1) (term t2)
          | Subset -> Z3.Set.mk_subset context (term t1) (term t2)
          | LTPointer ->
+            (* FIXME this needs to check whether alloc_ids are equal *)
             Z3.Arithmetic.mk_lt context (loc_to_integer (term t1))
               (loc_to_integer (term t2))
          | LEPointer ->
+            (* FIXME this needs to check whether alloc_ids are equal *)
             Z3.Arithmetic.mk_le context (loc_to_integer (term t1))
               (loc_to_integer (term t2))
          | And -> Z3.Boolean.mk_and context (map term [t1;t2])

diff --git a/tests/cn/append.c b/tests/cn/append.c
@@ -21,7 +21,7 @@ function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
 }
 
 predicate (datatype seq) IntList(pointer p) {
-  if (p == NULL) { 
+  if (is_null(p)) { 
     return Seq_Nil{};
   } else { 
     take H = Owned<struct int_list>(p);

diff --git a/tests/cn/fun_ptr_extern.c b/tests/cn/fun_ptr_extern.c
@@ -24,7 +24,7 @@ int_binop g1 = f2;
 
 /*@
 predicate {integer x} Is_Known_Binop (pointer f) {
-  assert ((f == &f1) || (f == &f2));
+  assert (ptr_eq(f, &f1) || ptr_eq(f, &f2));
   return {x: 1};
 }
 @*/

diff --git a/tests/cn/list_rev01.c b/tests/cn/list_rev01.c
@@ -7,7 +7,7 @@ struct node {
 
 /*@
 predicate {integer len} List (pointer p) {
-  if ( p == NULL ) {
+  if ( is_null(p) ) {
     return { len: 0 };
   }
   else {

diff --git a/tests/cn/mergesort.c b/tests/cn/mergesort.c
@@ -10,7 +10,7 @@ datatype seq {
 }
 
 predicate (datatype seq) IntList(pointer p) {
-  if (p == NULL) { 
+  if (is_null(p)) { 
     return Seq_Nil{};
   } else { 
     take H = Owned<struct int_list>(p);

diff --git a/tests/cn/mutual_rec/mutual_rec.c b/tests/cn/mutual_rec/mutual_rec.c
@@ -43,7 +43,7 @@ datatype b_tree {
 
 /*@
 predicate {datatype a_tree t} A_Tree (pointer p) {
-  if (p == NULL) {
+  if (is_null(p)) {
     return {t: A_Leaf {}};
   }
   else {
@@ -55,7 +55,7 @@ predicate {datatype a_tree t} A_Tree (pointer p) {
 }
 
 predicate {datatype b_tree t} B_Tree (pointer p) {
-  if (p == NULL) {
+  if (is_null(p)) {
     return {t: B_Leaf {}};
   }
   else {
@@ -107,7 +107,7 @@ struct a_node *
 predef_a_tree (struct a_node *p)
 /*@ requires take T = A_Tree (p) @*/
 /*@ ensures take T2 = A_Tree (p) @*/
-/*@ ensures (return == NULL) || (T2.t == A_Node {k: 1, v: 0,
+/*@ ensures is_null(return) || (T2.t == A_Node {k: 1, v: 0,
     left: B_Node {even: A_Leaf {}, odd: A_Leaf {}}, right: B_Leaf {}}) @*/
 {
   struct b_node *l = NULL;

diff --git a/tests/cn/pred_def01.c b/tests/cn/pred_def01.c
@@ -33,7 +33,7 @@ datatype int_list {
 }
 
 predicate {datatype int_list v} IntList(pointer l) {
-  if ( l == NULL ) {
+  if ( is_null(l) ) {
     return { v: Nil {} } ;
   } else {
     take H = Owned<struct int_list_items>(l) ;

diff --git a/tests/cn/pred_def02.c b/tests/cn/pred_def02.c
@@ -5,7 +5,7 @@ struct int_list_items {
 
 /*@
 predicate {integer len} IntList(pointer l) {
-  if ( l == NULL ) {
+  if ( is_null(l) ) {
     return { len: 0 } ;
   } else {
     take Head_item = Owned<struct int_list_items>(l) ;

diff --git a/tests/cn/pred_def03.error.c b/tests/cn/pred_def03.error.c
@@ -5,7 +5,7 @@ struct int_list_items {
 
 /*@
 predicate {integer len} IntList(pointer l) {
-  if ( l == NULL ) {
+  if ( is_null(l) ) {
     return { len: 0 } ;
   } else {
     take head_item = Owned<struct int_list_items>(l) ;

diff --git a/tests/cn/test_pointer_eq.c b/tests/cn/test_pointer_eq.c
@@ -4,5 +4,5 @@ void f (int *p)
 {
   unsigned long long p_int = (unsigned long long) p;
   int* q = __cerbvar_copy_alloc_id(p_int + 0ULL, p);
-  /*@ assert (p == q); @*/
+  /*@ assert (ptr_eq(p, q)); @*/
 }
diff --git a/tests/cn/tree16/as_auto_mutual_dt/tree16.c b/tests/cn/tree16/as_auto_mutual_dt/tree16.c
@@ -34,7 +34,7 @@ function (map <integer, datatype tree>) default_children ()
 predicate {datatype tree t, integer v, map <integer, datatype tree> children}
   Tree (pointer p)
 {
-  if (p == NULL) {
+  if (is_null(p)) {
     return {t: Empty_Tree {}, v: 0, children: default_children ()};
   }
   else {

diff --git a/tests/cn/tree16/as_mutual_dt/tree16.c b/tests/cn/tree16/as_mutual_dt/tree16.c
@@ -41,7 +41,7 @@ function (map <integer, datatype tree>) default_children ()
 predicate {datatype tree t, integer v, map <integer, datatype tree> children}
   Tree (pointer p)
 {
-  if (p == NULL) {
+  if (is_null(p)) {
     return {t: Empty_Tree {}, v: 0, children: default_children ()};
   }
   else {

diff --git a/tests/cn/tree16/as_partial_map/tree16.c b/tests/cn/tree16/as_partial_map/tree16.c
@@ -44,7 +44,7 @@ predicate {map<datatype tree_arc, datatype tree_node_option> t,
         integer v, map<integer, map<datatype tree_arc, datatype tree_node_option> > ns}
   Tree (pointer p)
 {
-  if (p == NULL) {
+  if (is_null(p)) {
     return {t: (empty ()), v: 0, ns: default_ns ()};
   }
   else {

diff --git a/tests/cn/tree_rev01.c b/tests/cn/tree_rev01.c
@@ -8,7 +8,7 @@ struct tree_node {
 
 /*@
 predicate {integer size} Tree (pointer p) {
-  if ( p == NULL ) {
+  if (is_null(p)) {
     return { size: 0 };
   }
   else {