CN VIP: Improve err msg for live alloc bound-check

Author: dc-mak

backend/cn/lib/check.ml

@@ -450,7 +450,7 @@ let check_alloc_bounds loc ~ptr ub_unspec =
       let@ model = model () in
       let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
       fail (fun ctxt ->
-        { loc; msg = Alloc_out_of_bounds { constr; ptr; ub; ctxt; model } }))
+        { loc; msg = Alloc_out_of_bounds { constr; term = ptr; ub; ctxt; model } }))
   else
     return ()
 
@@ -473,7 +473,7 @@ let check_both_eq_alloc loc arg1 arg2 ub =
   | `True -> return ()
 
 
-let check_live_alloc_bounds reason loc arg ub constr =
+let check_live_alloc_bounds reason loc arg ub term constr =
   let@ base_size = RI.Special.get_live_alloc reason loc arg in
   let here = Locations.other __FUNCTION__ in
   let base, size = Alloc.History.get_base_size base_size here in
@@ -484,7 +484,8 @@ let check_live_alloc_bounds reason loc arg ub constr =
     | `True -> return ()
     | `False ->
       let@ model = model () in
-      fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))
+      fail (fun ctxt ->
+        { loc; msg = Alloc_out_of_bounds { term; constr; ub; ctxt; model } }))
   else
     return ()
 
@@ -1382,7 +1383,13 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
            check_pexpr pe2 (fun arg2 ->
              let@ () = check_both_eq_alloc loc arg1 arg2 ub in
              let@ () =
-               check_live_alloc_bounds `Ptr_cmp loc arg1 ub (both_in_bounds arg1 arg2)
+               check_live_alloc_bounds
+                 `Ptr_cmp
+                 loc
+                 arg1
+                 ub
+                 (IT.tuple_ [ arg1; arg2 ] here)
+                 (both_in_bounds arg1 arg2)
              in
              k (op (arg1, arg2))))
        in
@@ -1411,7 +1418,13 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
               let ub_unspec = CF.Undefined.UB_unspec_pointer_sub in
               let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
               let@ () =
-                check_live_alloc_bounds `Ptr_diff loc arg1 ub (both_in_bounds arg1 arg2)
+                check_live_alloc_bounds
+                  `Ptr_diff
+                  loc
+                  arg1
+                  ub
+                  (IT.tuple_ [ arg1; arg2 ] here)
+                  (both_in_bounds arg1 arg2)
               in
               let ptr_diff_bt = Memory.bt_of_sct (Integer Ptrdiff_t) in
               let value =
@@ -1510,11 +1523,17 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
               let@ () = check_has_alloc_id loc vt1 ub_unspec in
               let here = Locations.other __FUNCTION__ in
               let@ () =
-                check_live_alloc_bounds `ISO_array_shift loc vt1 ub (fun ~base ~size ->
-                  let addr = addr_ result here in
-                  let lower = le_ (base, addr) here in
-                  let upper = le_ (addr, add_ (base, size) here) here in
-                  and_ [ lower; upper ] here)
+                check_live_alloc_bounds
+                  `ISO_array_shift
+                  loc
+                  vt1
+                  ub
+                  result
+                  (fun ~base ~size ->
+                     let addr = addr_ result here in
+                     let lower = le_ (base, addr) here in
+                     let upper = le_ (addr, add_ (base, size) here) here in
+                     and_ [ lower; upper ] here)
               in
               k result))
         | PtrMemberShift (_tag_sym, _memb_ident, _pe) ->
@@ -1535,7 +1554,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
               let@ () = check_has_alloc_id loc vt2 ub_unspec in
               let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
               let@ () =
-                check_live_alloc_bounds `Copy_alloc_id loc vt2 ub (fun ~base ~size ->
+                check_live_alloc_bounds `Copy_alloc_id loc vt2 ub vt1 (fun ~base ~size ->
                   let addr = vt1 in
                   let lower = le_ (base, addr) here in
                   let upper = le_ (addr, add_ (base, size) here) here in

backend/cn/lib/typeErrors.ml

@@ -205,7 +205,7 @@ type message =
         model : Solver.model_with_q
       }
   | Alloc_out_of_bounds of
-      { ptr : IT.t;
+      { term : IT.t;
         constr : IT.t;
         ub : CF.Undefined.undefined_behaviour;
         ctxt : Context.t * log;
@@ -508,8 +508,8 @@ let pp_message te =
       | None -> !^(CF.Undefined.ub_short_string ub)
     in
     { short; descr = Some descr; state = Some state }
-  | Alloc_out_of_bounds { constr; ptr; ub; ctxt; model } ->
-    let short = !^"Pointer " ^^ bquotes (IT.pp ptr) ^^ !^" out of bounds" in
+  | Alloc_out_of_bounds { constr; term; ub; ctxt; model } ->
+    let short = bquotes (IT.pp term) ^^ !^" out of bounds" in
     let state =
       trace ctxt model Explain.{ no_ex with unproven_constraint = Some (LC.T constr) }
     in