CN: Add NULL constr to solver mapping for ptrs

This is to more closely match VIP and also probably remove the need to
specify `is_null(x) || !addr_eq(x, NULL` which is just silly.

This uses match (for future-proofing against the addition of a `funcptr`
constructor) and default<loc> for morally partial index terms. It
also rejects more programs as a result.

HasAllocId is a positive way to check that a pointer is in the `(@i, a)`
datatype case rather than not NULL. Whilst the two are equivalent right
now, this change is is mainly to future-proof against the addition of
`funcptr` constructor for function pointers as in VIP/PNVI-*.

The implementation relies on a few design choices:
1. Shifting on NULL is forbidden (implicitly) by the ISO C standard (it
   requires pointers which point to objects, hence cannot be NULL).
   Also, we believe real-world code only relies on this idiom for
   hand-implementing `offsetof`, so we forbid it. This is enforced in
   the typing rules.

2. It doesn't enforce that NULL is the same as/has address 0, although
   if need be, the implementation could use this info since no known
   optimisations/compilers etc. rely on NULL not being 0. Note that
   casting 0 to a pointer gives NULL, and casting a NULL pointer to an
   integer gives 0.

3. Shifting NULL in the specification language results in
   `default<Loc>`. Representing it as an provenance-address pair with an
   empty provenance would also be fine but would raise further questions
   on how to represent the empty provenance (an unconstrained variable,
   or a special value, the latter of which would require constraints on
   all Owned pointers to not have that special value as their
   provenance). For any choice here, one could construct a program in
   which proof and runtime testing diverge.

4. `each (u64 i; ..) { Owned(array_shift(p,i); }` is defined to imply
   `has_alloc_id(p)`.

5. Addresses of global variables are also constrained with
  `has_alloc_id(&global)`.

It uses SMT functions for a more readable SMT file output. Unfortunately
it also triggers: Z3Prover/z3#7352 which is
worked-around by using modifying the simplifier and calling it at
exactly the right moment (comments in the code). The test for this
is added in tests/cn/simplify_array_shift.c

backend/cn/lib/builtins.ml

@@ -141,6 +141,13 @@ let is_null_def =
       IT.sterm_of_term IT.(eq_ (IT.term_of_sterm p, null_ loc') loc')) )
 
 
+let has_alloc_id_def =
+  ( "has_alloc_id",
+    Sym.fresh_named "has_alloc_id",
+    mk_arg1 (fun p loc' -> IT.sterm_of_term @@ IT.hasAllocId_ (IT.term_of_sterm p) loc')
+  )
+
+
 let ptr_eq_def =
   ( "ptr_eq",
     Sym.fresh_named "ptr_eq",
@@ -154,10 +161,8 @@ let prov_eq_def =
     mk_arg2 (fun (p1, p2) loc' ->
       IT.(
         sterm_of_term
-        @@ eq_
-             ( pointerToAllocIdCast_ (term_of_sterm p1) loc',
-               pointerToAllocIdCast_ (term_of_sterm p2) loc' )
-             loc')) )
+        @@ eq_ (allocId_ (term_of_sterm p1) loc', allocId_ (term_of_sterm p2) loc') loc'))
+  )
 
 
 let addr_eq_def =
@@ -166,10 +171,7 @@ let addr_eq_def =
     mk_arg2 (fun (p1, p2) loc' ->
       IT.(
         sterm_of_term
-        @@ eq_
-             ( pointerToIntegerCast_ (term_of_sterm p1) loc',
-               pointerToIntegerCast_ (term_of_sterm p2) loc' )
-             loc')) )
+        @@ eq_ (addr_ (term_of_sterm p1) loc', addr_ (term_of_sterm p2) loc') loc')) )
 
 
 let max_min_bits =
@@ -208,6 +210,7 @@ let builtin_funs =
       nth_list_def;
       array_to_list_def;
       is_null_def;
+      has_alloc_id_def;
       prov_eq_def;
       ptr_eq_def;
       addr_eq_def

backend/cn/lib/cLogicalFuns.ml

@@ -57,7 +57,7 @@ let init_state = { loc_map = IntMap.empty; next_loc = 1 }
 let mk_local_ptr state src_loc =
   let loc_ix = state.next_loc in
   let here = Locations.other __FUNCTION__ in
-  let ptr = IT.pred_ local_sym_ptr [ IT.int_ loc_ix here ] BT.Loc src_loc in
+  let ptr = IT.apply_ local_sym_ptr [ IT.int_ loc_ix here ] BT.Loc src_loc in
   let loc_map = IntMap.add loc_ix None state.loc_map in
   let state = { loc_map; next_loc = loc_ix + 1 } in
   (ptr, state)
@@ -548,7 +548,7 @@ let rec symb_exec_mu_expr ctxt state_vars expr =
     if SymMap.mem nm ctxt.c_fun_pred_map then (
       let loc, l_sym = SymMap.find nm ctxt.c_fun_pred_map in
       let@ def = get_logical_function_def loc l_sym in
-      rcval (IT.pred_ l_sym args_its def.LogicalFunctions.return_bt loc) state)
+      rcval (IT.apply_ l_sym args_its def.LogicalFunctions.return_bt loc) state)
     else if Sym.has_id_with Setup.unfold_stdlib_name nm then (
       let s = Option.get (Sym.has_id nm) in
       let wrap_int x = IT.wrapI_ (signed_int_ity, x) in

backend/cn/lib/check.ml

@@ -410,12 +410,6 @@ let check_conv_int loc ~expect ct arg =
   return value
 
 
-let _check_array_shift loc ~expect vt1 (loc_ct, ct) vt2 =
-  let@ () = WellTyped.ensure_base_type loc ~expect Loc in
-  let@ () = WellTyped.WCT.is_ct loc_ct ct in
-  return (arrayShift_ ~base:vt1 ct ~index:vt2)
-
-
 let check_against_core_bt loc msg2 cbt bt =
   Typing.embed_resultat
     (CoreTypeChecks.check_against_core_bt
@@ -424,6 +418,16 @@ let check_against_core_bt loc msg2 cbt bt =
        bt)
 
 
+let check_has_alloc_id loc k ~ptr ~result ub_unspec =
+  let@ provable = provable loc in
+  match provable (t_ (hasAllocId_ ptr loc)) with
+  | `True -> k result
+  | `False ->
+    let@ model = model () in
+    let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
+    fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })
+
+
 let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m =
   let orig_pe = pe in
   let (M_Pexpr (loc, _, expect, pe_)) = pe in
@@ -522,13 +526,17 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m =
        let@ () = WellTyped.ensure_bits_type loc (bt_of_pexpr pe2) in
        check_pexpr pe1 (fun vt1 ->
          check_pexpr pe2 (fun vt2 ->
-           k (arrayShift_ ~base:vt1 ct ~index:(cast_ Memory.uintptr_bt vt2 loc) loc)))
+           let result =
+             arrayShift_ ~base:vt1 ct ~index:(cast_ Memory.uintptr_bt vt2 loc) loc
+           in
+           check_has_alloc_id loc k ~ptr:vt1 ~result CF.Undefined.UB_unspec_pointer_add))
      | M_PEmember_shift (pe, tag, member) ->
        let@ () = WellTyped.ensure_base_type loc ~expect Loc in
        let@ () = ensure_base_type loc ~expect:Loc (bt_of_pexpr pe) in
        check_pexpr pe (fun vt ->
          let@ _ = get_struct_member_type loc tag member in
-         k (memberShift_ (vt, tag, member) loc))
+         let result = memberShift_ (vt, tag, member) loc in
+         check_has_alloc_id loc k ~ptr:vt ~result CF.Undefined.UB_unspec_pointer_add)
      | M_PEnot pe ->
        let@ () = WellTyped.ensure_base_type loc ~expect Bool in
        let@ () = ensure_base_type loc ~expect:Bool (bt_of_pexpr pe) in
@@ -1204,45 +1212,74 @@ let rec check_expr labels (e : BT.t mu_expr) (k : IT.t -> unit m) : unit m =
      | M_Ememop memop ->
        let here = Locations.other __FUNCTION__ in
        let pointer_eq ?(negate = false) pe1 pe2 =
+         let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+         let k, case, res =
+           if negate then ((fun x -> k (not_ x loc)), "in", "ptrNeq") else (k, "", "ptrEq")
+         in
          check_pexpr pe1 (fun arg1 ->
            check_pexpr pe2 (fun arg2 ->
-             let prov1, prov2 =
-               (pointerToAllocIdCast_ arg1 here, pointerToAllocIdCast_ arg2 here)
+             let bind name term =
+               let sym, it = IT.fresh_named Bool name loc in
+               let@ _ = add_a sym Bool (here, lazy (Sym.pp sym)) in
+               let@ () = add_c loc (LC.t_ (term it)) in
+               return it
              in
-             let addr1, addr2 =
-               (pointerToIntegerCast_ arg1 here, pointerToIntegerCast_ arg2 here)
+             let@ ambiguous =
+               bind "ambiguous"
+               @@ fun ambiguous ->
+               eq_
+                 ( ambiguous,
+                   and_
+                     [ hasAllocId_ arg1 here;
+                       hasAllocId_ arg2 here;
+                       ne_ (allocId_ arg1 here, allocId_ arg2 here) here;
+                       eq_ (addr_ arg1 here, addr_ arg2 here) here
+                     ]
+                     here )
+                 here
              in
-             let addr_eq = eq_ (addr1, addr2) loc in
-             let prov_eq = eq_ (prov1, prov2) loc in
-             let prov_neq = ne_ (prov1, prov2) loc in
              let@ provable = provable loc in
              let@ () =
-               match provable @@ t_ @@ and_ [ prov_neq; addr_eq ] here with
+               match provable @@ t_ ambiguous with
                | `False -> return ()
                | `True ->
-                 warn
-                   loc
-                   !^"ambiguous pointer (in)equality case: addresses equal, but \
-                      provenances differ";
+                 let msg =
+                   Printf.sprintf
+                     "ambiguous pointer %sequality case: addresses equal, but \
+                      provenances differ"
+                     case
+                 in
+                 warn loc !^msg;
                  return ()
              in
-             let res_sym, res =
-               IT.fresh_named Bool (if negate then "ptrNeq" else "ptrEq") loc
+             let@ both_eq =
+               bind "both_eq" @@ fun both_eq -> eq_ (both_eq, eq_ (arg1, arg2) here) here
              in
-             let@ _result = add_a res_sym Bool (loc, lazy (Sym.pp res_sym)) in
-             let@ () = add_c loc @@ t_ @@ impl_ (prov_eq, eq_ (res, addr_eq) loc) loc in
-             (* this constraint may make the result non-deterministic *)
-             let@ () =
-               add_c loc
-               @@ t_
-               @@ impl_
-                    ( prov_neq,
-                      or_ [ eq_ (res, addr_eq) loc; eq_ (res, bool_ false here) loc ] loc
-                    )
-                    loc
+             let@ neither =
+               bind "neither"
+               @@ fun neither ->
+               eq_ (neither, and_ [ not_ both_eq here; not_ ambiguous here ] here) here
              in
-             let@ () = WellTyped.ensure_base_type loc ~expect (IT.bt res) in
-             k (if negate then not_ res loc else res)))
+             let@ res =
+               bind res
+               @@ fun res ->
+               (* NOTE: ambiguous case is intentionally under-specified *)
+               and_ [ impl_ (both_eq, res) here; impl_ (neither, not_ res here) here ] loc
+             in
+             k res
+             (* (* TODO: use this if SW_strict_pointer_equality is enabled *)
+                k
+                (or_
+                [ and_ [ eq_ (null_ here, arg1) here; eq_ (null_ here, arg2) here ] here;
+                       and_
+                         [ hasAllocId_ arg1 here;
+                           hasAllocId_ arg2 here;
+                           eq_ (addr_ arg1 here, addr_ arg2 here) here
+                         ]
+                         here
+                     ]
+                here)
+             *)))
        in
        let pointer_op op pe1 pe2 =
          let@ () = ensure_base_type loc ~expect Bool in
@@ -1270,21 +1307,26 @@ let rec check_expr labels (e : BT.t mu_expr) (k : IT.t -> unit m) : unit m =
                 | Array (item_ty, _) -> Memory.size_of_ctype item_ty
                 | ct -> Memory.size_of_ctype ct
               in
-              let ptr_diff_bt = Memory.bt_of_sct (Integer Ptrdiff_t) in
-              let value =
-                (* TODO: confirm that the cast from uintptr_t to ptrdiff_t
-                   yields the expected result. *)
-                div_
-                  ( cast_
-                      ptr_diff_bt
-                      (sub_
-                         (pointerToIntegerCast_ arg1 loc, pointerToIntegerCast_ arg2 loc)
-                         loc)
-                      loc,
-                    int_lit_ divisor ptr_diff_bt loc )
-                  loc
+              let both_alloc =
+                and_ [ hasAllocId_ arg1 here; hasAllocId_ arg2 here ] here
               in
-              k value))
+              let@ provable = provable loc in
+              match provable @@ t_ @@ both_alloc with
+              | `False ->
+                let@ model = model () in
+                let ub = CF.Undefined.(UB_CERB004_unspecified UB_unspec_pointer_sub) in
+                fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })
+              | `True ->
+                let ptr_diff_bt = Memory.bt_of_sct (Integer Ptrdiff_t) in
+                let value =
+                  (* TODO: confirm that the cast from uintptr_t to ptrdiff_t
+                     yields the expected result. *)
+                  div_
+                    ( cast_ ptr_diff_bt (sub_ (addr_ arg1 loc, addr_ arg2 loc) loc) loc,
+                      int_lit_ divisor ptr_diff_bt loc )
+                    loc
+                in
+                k value))
         | M_IntFromPtr (act_from, act_to, pe) ->
           let@ () = WellTyped.WCT.is_ct act_from.loc act_from.ct in
           let@ () = WellTyped.WCT.is_ct act_to.loc act_to.ct in
@@ -1346,7 +1388,11 @@ let rec check_expr labels (e : BT.t mu_expr) (k : IT.t -> unit m) : unit m =
           let@ () = WellTyped.WCT.is_ct act.loc act.ct in
           let@ () = WellTyped.ensure_bits_type loc (bt_of_pexpr pe2) in
           check_pexpr pe1 (fun vt1 ->
-            check_pexpr pe2 (fun vt2 -> k (arrayShift_ ~base:vt1 act.ct ~index:vt2 loc)))
+            check_pexpr pe2 (fun vt2 ->
+              let result =
+                arrayShift_ ~base:vt1 ~index:(cast_ Memory.uintptr_bt vt2 loc) act.ct loc
+              in
+              check_has_alloc_id loc k ~ptr:vt1 ~result CF.Undefined.UB_unspec_pointer_add))
         | M_PtrMemberShift (_tag_sym, _memb_ident, _pe) ->
           (* FIXME(CHERI merge) *)
           (* there is now an effectful variant of the member shift operator (which is UB when creating an out of bound pointer) *)
@@ -1357,7 +1403,14 @@ let rec check_expr labels (e : BT.t mu_expr) (k : IT.t -> unit m) : unit m =
           in
           let@ () = WellTyped.ensure_base_type loc ~expect:BT.Loc (bt_of_pexpr pe2) in
           check_pexpr pe1 (fun vt1 ->
-            check_pexpr pe2 (fun vt2 -> k (copyAllocId_ ~addr:vt1 ~loc:vt2 loc)))
+            check_pexpr pe2 (fun vt2 ->
+              let result = copyAllocId_ ~addr:vt1 ~loc:vt2 loc in
+              check_has_alloc_id
+                loc
+                k
+                ~ptr:vt2
+                ~result
+                CF.Undefined.UB_unspec_copy_alloc_id))
         | M_Memcpy _ (* (asym 'bty * asym 'bty * asym 'bty) *) ->
           Cerb_debug.error "todo: M_Memcpy"
         | M_Memcmp _ (* (asym 'bty * asym 'bty * asym 'bty) *) ->
@@ -1648,7 +1701,7 @@ let rec check_expr labels (e : BT.t mu_expr) (k : IT.t -> unit m) : unit m =
               in
               fail (fun _ -> { loc; msg = Generic msg })
             | Some body ->
-              add_c loc (LC.t_ (eq_ (pred_ f args def.return_bt loc, body) loc)))
+              add_c loc (LC.t_ (eq_ (apply_ f args def.return_bt loc, body) loc)))
          | M_CN_apply (lemma, args) ->
            let@ _loc, lemma_typ = get_lemma loc lemma in
            let args = List.map (fun arg -> (loc, arg)) args in
@@ -1968,6 +2021,7 @@ let record_globals : 'bty. (symbol * 'bty mu_globs) list -> unit m =
         let@ () =
           add_c here (t_ (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt, here)) here))
         in
+        let@ () = add_c here (t_ (IT.hasAllocId_ (sym_ (sym, bt, here)) here)) in
         return ())
     globs
 

backend/cn/lib/cn_internal_to_ail.ml

@@ -1191,6 +1191,7 @@ let rec cn_to_ail_expr_aux_internal
     in
     dest d (b1 @ b2, s1 @ s2, mk_expr ail_expr_)
   | CopyAllocId _ -> failwith "TODO CopyAllocId"
+  | HasAllocId _ -> failwith "TODO HasAllocId"
   | Nil bt -> failwith "TODO8"
   | Cons (x, xs) -> failwith "TODO9"
   | Head xs ->

backend/cn/lib/compile.ml

@@ -856,7 +856,7 @@ module EffectfulTranslation = struct
                fail
                  { loc; msg = Unknown_logical_function { id = fsym; resource = false } }
            in
-           return (pred_ fsym args (SurfaceBaseTypes.of_basetype bt) loc))
+           return (apply_ fsym args (SurfaceBaseTypes.of_basetype bt) loc))
       | CNExpr_cons (c_nm, exprs) ->
         let@ cons_info = lookup_constr loc c_nm env in
         let@ exprs =

backend/cn/lib/indexTerms.ml

@@ -76,6 +76,7 @@ let rec free_vars_bts (it : 'a term) : BT.t SymMap.t =
   | MemberShift (t, _tag, _id) -> free_vars_bts t
   | ArrayShift { base; ct = _; index } -> free_vars_bts_list [ base; index ]
   | CopyAllocId { addr; loc } -> free_vars_bts_list [ addr; loc ]
+  | HasAllocId loc -> free_vars_bts_list [ loc ]
   | SizeOf _t -> SymMap.empty
   | OffsetOf (_tag, _member) -> SymMap.empty
   | Nil _bt -> SymMap.empty
@@ -175,6 +176,7 @@ let rec fold_ f binders acc = function
   | MemberShift (t, _tag, _id) -> fold f binders acc t
   | ArrayShift { base; ct = _; index } -> fold_list f binders acc [ base; index ]
   | CopyAllocId { addr; loc } -> fold_list f binders acc [ addr; loc ]
+  | HasAllocId loc -> fold_list f binders acc [ loc ]
   | SizeOf _ct -> acc
   | OffsetOf (_tag, _member) -> acc
   | Nil _bt -> acc
@@ -300,6 +302,7 @@ let rec subst (su : [ `Term of typed | `Rename of Sym.t ] subst) (IT (it, bt, lo
     IT (ArrayShift { base = subst su base; ct; index = subst su index }, bt, loc)
   | CopyAllocId { addr; loc = ptr } ->
     IT (CopyAllocId { addr = subst su addr; loc = subst su ptr }, bt, loc)
+  | HasAllocId ptr -> IT (HasAllocId (subst su ptr), bt, loc)
   | SizeOf t -> IT (SizeOf t, bt, loc)
   | OffsetOf (tag, member) -> IT (OffsetOf (tag, member), bt, loc)
   | Aligned t -> IT (Aligned { t = subst su t.t; align = subst su t.align }, bt, loc)
@@ -712,10 +715,10 @@ let uintptr_const_ n loc = num_lit_ n Memory.uintptr_bt loc
 let uintptr_int_ n loc = uintptr_const_ (Z.of_int n) loc
 (* for integer-mode: z_ n *)
 
-let pointerToIntegerCast_ it loc = cast_ Memory.uintptr_bt it loc
+let addr_ it loc = cast_ Memory.uintptr_bt it loc
 (* for integer-mode: cast_ Integer it *)
 
-let pointerToAllocIdCast_ it loc = cast_ Alloc_id it loc
+let allocId_ it loc = cast_ Alloc_id it loc
 
 let memberShift_ (base, tag, member) loc =
   IT (MemberShift (base, tag, member), BT.Loc, loc)
@@ -725,6 +728,8 @@ let arrayShift_ ~base ~index ct loc = IT (ArrayShift { base; ct; index }, BT.Loc
 
 let copyAllocId_ ~addr ~loc:ptr loc = IT (CopyAllocId { addr; loc = ptr }, BT.Loc, loc)
 
+let hasAllocId_ ptr loc = IT (HasAllocId ptr, BT.Bool, loc)
+
 let sizeOf_ ct loc = IT (SizeOf ct, Memory.size_bt, loc)
 
 let isIntegerToPointerCast = function
@@ -824,7 +829,7 @@ let make_array_ ~index_bt ~item_bt items (* assumed all of item_bt *) loc =
   value
 
 
-let pred_ name args rbt loc = IT (Apply (name, args), rbt, loc)
+let apply_ name args rbt loc = IT (Apply (name, args), rbt, loc)
 
 (* let let_ sym e body = *)
 (*   subst (make_subst [(sym, e)]) body *)
@@ -904,15 +909,15 @@ let const_of_c_sig (c_sig : Sctypes.c_concrete_sig) loc =
 
 
 (* let _non_vip_constraint about loc =  *)
-(*   eq_ (pointerToAllocIdCast_ about loc, alloc_id_ Z.zero loc) loc *)
+(*   eq_ (allocId_ about loc, alloc_id_ Z.zero loc) loc *)
 
 (* TODO: are the constraints `0<about` and `about+pointee_size-1 <= max-pointer`
    required? *)
 let value_check_pointer mode ~pointee_ct about loc =
   match mode with
   | `Representable -> bool_ true loc
   | `Good ->
-    (* let about_int = pointerToIntegerCast_ about loc in *)
+    (* let about_int = addr_ about loc in *)
     (* let pointee_size = match pointee_ct with *)
     (*   | Sctypes.Void -> 1 *)
     (*   | Function _ -> 1 *)