From af5abdb2e4a03fdc38bd6e5625d410c7f038a97b Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Wed, 8 Nov 2023 13:48:59 +0000 Subject: [PATCH] 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". --- backend/cn/builtins.ml | 27 ++++++++++++++++++---- backend/cn/compile.ml | 12 +++++++++- backend/cn/solver.ml | 2 ++ tests/cn/append.c | 2 +- tests/cn/fun_ptr_extern.c | 2 +- tests/cn/list_rev01.c | 2 +- tests/cn/mergesort.c | 2 +- tests/cn/mutual_rec/mutual_rec.c | 6 ++--- tests/cn/pred_def01.c | 2 +- tests/cn/pred_def02.c | 2 +- tests/cn/pred_def03.error.c | 2 +- tests/cn/test_pointer_eq.c | 2 +- tests/cn/tree16/as_auto_mutual_dt/tree16.c | 2 +- tests/cn/tree16/as_mutual_dt/tree16.c | 2 +- tests/cn/tree16/as_partial_map/tree16.c | 2 +- tests/cn/tree_rev01.c | 2 +- 16 files changed, 51 insertions(+), 20 deletions(-) diff --git a/backend/cn/builtins.ml b/backend/cn/builtins.ml index 9dc075e99..3da706d3f 100644 --- 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 index a478b4814..26cf53246 100644 --- 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 index f44544540..bd11ed436 100644 --- 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 index d1d518402..876436b91 100644 --- 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(p); diff --git a/tests/cn/fun_ptr_extern.c b/tests/cn/fun_ptr_extern.c index e73dcd870..35607d822 100644 --- 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 index f7a1319cb..267cf6925 100644 --- 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 index 61f312d0f..25f9fa2fc 100644 --- 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(p); diff --git a/tests/cn/mutual_rec/mutual_rec.c b/tests/cn/mutual_rec/mutual_rec.c index 3ebbdb255..b629e6677 100644 --- 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 index 1794608c1..f027eaede 100644 --- 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(l) ; diff --git a/tests/cn/pred_def02.c b/tests/cn/pred_def02.c index 2a2f3614c..799308aa4 100644 --- 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(l) ; diff --git a/tests/cn/pred_def03.error.c b/tests/cn/pred_def03.error.c index f2ae7a584..7d611e33f 100644 --- 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(l) ; diff --git a/tests/cn/test_pointer_eq.c b/tests/cn/test_pointer_eq.c index 1f7bb5ade..7b82a7adc 100644 --- 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 index e622e45ab..cd4199ebd 100644 --- 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 ) default_children () predicate {datatype tree t, integer v, map 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 index 1d0d194f7..b78aecd40 100644 --- a/tests/cn/tree16/as_mutual_dt/tree16.c +++ b/tests/cn/tree16/as_mutual_dt/tree16.c @@ -41,7 +41,7 @@ function (map ) default_children () predicate {datatype tree t, integer v, map 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 index 98a841080..4994aac2e 100644 --- a/tests/cn/tree16/as_partial_map/tree16.c +++ b/tests/cn/tree16/as_partial_map/tree16.c @@ -44,7 +44,7 @@ predicate {map t, integer v, map > 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 index f1fe8fc5a..c0e024baf 100644 --- 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 {