CN: Fix tests (impl typing rules)

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
@@ -1206,18 +1214,18 @@ let rec check_expr labels (e : BT.t mu_expr) (k : IT.t -> unit m) : unit m =
        let pointer_eq ?(negate = false) pe1 pe2 =
          check_pexpr pe1 (fun arg1 ->
            check_pexpr pe2 (fun arg2 ->
-             let prov1, prov2 =
-               (pointerToAllocIdCast_ arg1 here, pointerToAllocIdCast_ arg2 here)
+             let 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
              in
-             let addr1, addr2 =
-               (pointerToIntegerCast_ arg1 here, pointerToIntegerCast_ arg2 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
@@ -1229,17 +1237,18 @@ let rec check_expr labels (e : BT.t mu_expr) (k : IT.t -> unit m) : unit m =
              let res_sym, res =
                IT.fresh_named Bool (if negate then "ptrNeq" else "ptrEq") loc
              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_a res_sym Bool (here, lazy (Sym.pp res_sym)) in
+             let both_eq = eq_ (arg1, arg2) here in
+             let neither = not_ (and_ [ both_eq; ambiguous ] here) here in
              let@ () =
                add_c loc
                @@ t_
-               @@ impl_
-                    ( prov_neq,
-                      or_ [ eq_ (res, addr_eq) loc; eq_ (res, bool_ false here) loc ] loc
-                    )
-                    loc
+               @@ and_
+                    [ impl_ (both_eq, eq_ (res, bool_ true here) here) here;
+                      impl_ (neither, eq_ (res, bool_ false here) here) here
+                      (* NOTE: ambiguous case is intentionally under-specified *)
+                    ]
+                    here
              in
              let@ () = WellTyped.ensure_base_type loc ~expect (IT.bt res) in
              k (if negate then not_ res loc else res)))
@@ -1270,21 +1279,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 +1360,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 +1375,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 +1673,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

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

@@ -715,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)
@@ -728,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
@@ -827,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 *)
@@ -907,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 *)

backend/cn/lib/lemmata.ml

@@ -421,7 +421,7 @@ let it_adjust (global : Global.t) it =
         t
       else
         f (IT.representable global.struct_decls ct t2 loc)
-    | Aligned t -> f (IT.divisible_ (IT.pointerToIntegerCast_ t.t loc, t.align) loc)
+    | Aligned t -> f (IT.divisible_ (IT.addr_ t.t loc, t.align) loc)
     | IT.Let ((nm, x), y) ->
       let x = f x in
       let y = f y in

backend/cn/lib/resourceInference.ml

@@ -197,18 +197,12 @@ module General = struct
         | P p', p'_oarg when RET.subsumed requested.name p'.name ->
           let here = Locations.other __FUNCTION__ in
           let pmatch =
-            eq_
-              ( (pointerToIntegerCast_ requested.pointer) here,
-                pointerToIntegerCast_ p'.pointer here )
-              here
+            eq_ ((addr_ requested.pointer) here, addr_ p'.pointer here) here
             :: List.map2 (fun x y -> eq__ x y here) requested.iargs p'.iargs
           in
           let took = and_ pmatch here in
           let prov =
-            eq_
-              ( pointerToAllocIdCast_ requested.pointer here,
-                pointerToAllocIdCast_ p'.pointer here )
-              here
+            eq_ (allocId_ requested.pointer here, allocId_ p'.pointer here) here
           in
           let debug_failure model msg term =
             Pp.debug 9 (lazy (Pp.item msg (RET.pp (fst re))));