CN VIP: Constrain global allocations

rems-project · Sep 26, 2024 · 68b0b09 · 68b0b09
1 parent e85a739
commit 68b0b09
Show file tree

Hide file tree

Showing 4 changed files with 41 additions and 4 deletions.
diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
@@ -446,7 +446,8 @@ let check_alloc_bounds loc ~ptr ub_unspec =
     | `False ->
       let@ model = model () in
       let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
-      fail (fun ctxt -> { loc; msg = Alloc_out_of_bounds { ptr; ub; ctxt; model } }))
+      fail (fun ctxt ->
+        { loc; msg = Alloc_out_of_bounds { constr; ptr; ub; ctxt; model } }))
   else
     return ()
 
@@ -2167,7 +2168,26 @@ let record_globals : 'bty. (Sym.t * 'bty Mu.mu_globs) list -> unit m =
         let@ () =
           add_c here (LC.T (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt, here)) here))
         in
-        let@ () = add_c here (LC.T (IT.hasAllocId_ (sym_ (sym, bt, here)) here)) in
+        let ptr = sym_ (sym, bt, here) in
+        let@ () = add_c here (LC.T (IT.hasAllocId_ ptr here)) in
+        let@ () =
+          if !IT.use_vip then (
+            let base_size = Alloc.History.lookup_ptr ptr here in
+            let base, size = Alloc.History.get_base_size base_size here in
+            let addr = addr_ ptr here in
+            let upper = Resources.upper_bound addr ct here in
+            let bounds =
+              and_
+                [ le_ (base, addr) here;
+                  le_ (addr, upper) here;
+                  le_ (upper, add_ (base, size) here) here
+                ]
+                here
+            in
+            add_c here (LC.T bounds))
+          else
+            return ()
+        in
         return ())
     globs
 

diff --git a/backend/cn/lib/typeErrors.ml b/backend/cn/lib/typeErrors.ml
@@ -209,6 +209,7 @@ type message =
       }
   | Alloc_out_of_bounds of
       { ptr : IT.t;
+        constr : IT.t;
         ub : CF.Undefined.undefined_behaviour;
         ctxt : Context.t * log;
         model : Solver.model_with_q
@@ -503,9 +504,11 @@ let pp_message te =
       | None -> !^(CF.Undefined.ub_short_string ub)
     in
     { short; descr = Some descr; state = Some state }
-  | Alloc_out_of_bounds { ptr; ub; ctxt; model } ->
+  | Alloc_out_of_bounds { constr; ptr; ub; ctxt; model } ->
     let short = !^"Pointer " ^^ bquotes (IT.pp ptr) ^^ !^" out of bounds" in
-    let state = trace ctxt model Explain.no_ex in
+    let state =
+      trace ctxt model Explain.{ no_ex with unproven_constraint = Some (LC.T constr) }
+    in
     let descr =
       match CF.Undefined.std_of_undefined_behaviour ub with
       | Some stdref -> !^(CF.Undefined.ub_short_string ub) ^^^ parens !^stdref

diff --git a/tests/cn/create_rdonly.c b/tests/cn/create_rdonly.c
@@ -0,0 +1,12 @@
+/*
+error: CreateReadOnly: not a constant ctype: Ivalignof('char[4]')
+	return "abc" == (void *)0;
+	       ^~~~~
+*/
+// Cause: constant string
+
+int
+main()
+{
+	return "abc" != (void *)0;
+}
diff --git a/tests/run-cn-exec.sh b/tests/run-cn-exec.sh
@@ -101,6 +101,7 @@ SUCCESS=$(find cn -name '*.c' \
     ! -name "ptr_relop.error.c" \
     ! -name "int_to_ptr.c" \
     ! -name "int_to_ptr.error.c" \
+    ! -name "create_rdonly.c" \
 )
 
 # Include files which cause error for proof but not testing
@@ -166,6 +167,7 @@ BUGGY="cn/division_casting.c \
        cn/ptr_relop.error.c \
        cn/int_to_ptr.c \
        cn/int_to_ptr.error.c \
+       cn/create_rdonly.c \
        "
 
 # Exclude files which cause error for proof but not testing