Use C-type (not index terms) for step in qpred

The previous commit introduce an error for a using array_shift on a void
pointer, but the location information was not useful. This was because
the array_shift was being deconstructed into a base pointer, and a
sizeof term, and the latter term, by virtue of being generated by CN
developers than the user, had an 'other' location. When this term was
later checked in wellTyped, it would error.

Feeling uncomfortable about lying about the origin and made-up nature of
the sizeof term, I instead did a long-overdue refactor of QPredicate.t
to have its "step" field just be a C-type instead of an arbitrary index
term.

I believe enough checks and errors about this have been in place about
this for long enough such that this is non-breaking change (and I also
ran the tests).

Author: dc-mak

Makefile

@@ -53,7 +53,7 @@ cn-coq:
 	$(Q)dune build -p cn-coq
 
 .PHONY: cn-coq-install
-cn-coq-install: install_lib cn-coq
+cn-coq-install: cn-coq
 	@echo "[DUNE] install cn-coq"
 	$(Q)dune install cn-coq
 

coq/Cn/Request.v

@@ -29,7 +29,7 @@ Module QPredicate.
     pointer : IndexTerms.t;
     q : Symbol.t * BaseTypes.t;
     q_loc : Locations.t;
-    step : IndexTerms.t;
+    step : SCtypes.ctype;
     permission : IndexTerms.t;
     iargs : list IndexTerms.t
   }.

lib/bugExplanation/replicators.ml

@@ -479,16 +479,7 @@ let compile_req
       let map_sym = Sym.fresh () in
       let b_val, s_val, e_val =
         aux
-          (P
-             { name;
-               pointer =
-                 IT.arrayShift_
-                   ~base:pointer
-                   ~index:(IT.mul_ (q_it, step) (IT.get_loc step))
-                   Sctypes.char_ct
-                   loc;
-               iargs
-             })
+          (P { name; pointer = IT.arrayShift_ ~base:pointer ~index:q_it step loc; iargs })
       in
       let s2 =
         A.

lib/bugExplanation/shapeAnalyzers.ml

@@ -198,16 +198,7 @@ let compile_req
       let map_sym = Sym.fresh () in
       let b_val, s_val, e_val =
         aux
-          (P
-             { name;
-               pointer =
-                 IT.arrayShift_
-                   ~base:pointer
-                   ~index:(IT.mul_ (q_it, step) (IT.get_loc step))
-                   Sctypes.char_ct
-                   loc;
-               iargs
-             })
+          (P { name; pointer = IT.arrayShift_ ~base:pointer ~index:q_it step loc; iargs })
       in
       let s2 =
         A.

lib/check.ml

@@ -1348,7 +1348,7 @@ let bytes_qpred sym size pointer init : Req.QPredicate.t =
   let bt' = WellTyped.default_quantifier_bt in
   { q = (sym, bt');
     q_loc = here;
-    step = IT.num_lit_ Z.one bt' here;
+    step = Sctypes.uchar_ct;
     permission = IT.(lt_ (sym_ (sym, bt', here), size) here);
     name = Owned (Sctypes.uchar_ct, init);
     pointer;

lib/cn_internal_to_ail.ml

@@ -2700,7 +2700,13 @@ let cn_to_ail_resource_internal
        Sym.fresh_pretty (Option.get (get_conversion_to_fn_str BT.Integer))
        in *)
     let b2, s2, _e2 = cn_to_ail_expr_internal dts globals q.permission PassBack in
-    let b3, s3, _e3 = cn_to_ail_expr_internal dts globals q.step PassBack in
+    let b3, s3, _e3 =
+      cn_to_ail_expr_internal
+        dts
+        globals
+        (IT.sizeOf_ q.step Cerb_location.unknown)
+        PassBack
+    in
     (* let conversion_fcall = A.(AilEcall (mk_expr (AilEident convert_to_cn_integer_sym), [e_start])) in *)
     let start_binding = create_binding i_sym cn_integer_ptr_ctype in
     let start_assign = A.(AilSdeclaration [ (i_sym, Some e_start) ]) in
@@ -2713,11 +2719,8 @@ let cn_to_ail_resource_internal
     let return_ctype, _return_bt = calculate_return_type q.name in
     (* Translation of q.pointer *)
     let i_it = IT.IT (IT.(Sym i_sym), i_bt, Cerb_location.unknown) in
-    let step_binop =
-      IT.IT (IT.(Binop (Mul, i_it, q.step)), i_bt, Cerb_location.unknown)
-    in
     let value_it =
-      IT.IT (IT.(Binop (Add, q.pointer, step_binop)), BT.(Loc ()), Cerb_location.unknown)
+      IT.arrayShift_ ~base:q.pointer ~index:i_it q.step Cerb_location.unknown
     in
     let b4, s4, e4 = cn_to_ail_expr_internal dts globals value_it PassBack in
     let ptr_add_sym = Sym.fresh () in
@@ -3830,7 +3833,13 @@ let cn_to_ail_assume_resource_internal
        Sym.fresh_pretty (Option.get (get_conversion_to_fn_str BT.Integer))
        in *)
     let b2, s2, _e2 = cn_to_ail_expr_internal dts globals q.permission PassBack in
-    let b3, s3, _e3 = cn_to_ail_expr_internal dts globals q.step PassBack in
+    let b3, s3, _e3 =
+      cn_to_ail_expr_internal
+        dts
+        globals
+        (IT.sizeOf_ q.step Cerb_location.unknown)
+        PassBack
+    in
     (* let conversion_fcall = A.(AilEcall (mk_expr (AilEident convert_to_cn_integer_sym), [e_start])) in *)
     let start_binding = create_binding i_sym cn_integer_ptr_ctype in
     let start_assign = A.(AilSdeclaration [ (i_sym, Some e_start) ]) in
@@ -3843,11 +3852,8 @@ let cn_to_ail_assume_resource_internal
     let return_ctype, _return_bt = calculate_return_type q.name in
     (* Translation of q.pointer *)
     let i_it = IT.IT (IT.(Sym i_sym), i_bt, Cerb_location.unknown) in
-    let step_binop =
-      IT.IT (IT.(Binop (Mul, i_it, q.step)), i_bt, Cerb_location.unknown)
-    in
     let value_it =
-      IT.IT (IT.(Binop (Add, q.pointer, step_binop)), BT.(Loc ()), Cerb_location.unknown)
+      IT.arrayShift_ ~base:q.pointer ~index:i_it q.step Cerb_location.unknown
     in
     let b4, s4, e4 = cn_to_ail_expr_internal dts globals value_it PassBack in
     let ptr_add_sym = Sym.fresh () in

lib/compile.ml

@@ -1142,8 +1142,7 @@ module EffectfulTranslation = struct
     let msg_s = "Iterated predicate pointer must be array_shift<ctype>(ptr, q_var):" in
     match IT.get_term ptr_expr with
     | ArrayShift { base = p; ct; index = x } when Terms.equal_annot SBT.equal x qs ->
-      let here = Locations.other __LOC__ in
-      return (p, IT.cast_ (SBT.proj bt) (IT.sizeOf_ ct here) here)
+      return (p, ct)
     | _ -> fail { loc; msg = Generic (!^msg_s ^^^ IT.pp ptr_expr) [@alert "-deprecated"] }
 
 

lib/executable_spec_records.ml

@@ -58,8 +58,7 @@ let rec add_records_to_map_from_it it =
 
 let add_records_to_map_from_resource = function
   | Request.P p -> List.iter add_records_to_map_from_it (p.pointer :: p.iargs)
-  | Q q ->
-    List.iter add_records_to_map_from_it (q.pointer :: q.step :: q.permission :: q.iargs)
+  | Q q -> List.iter add_records_to_map_from_it (q.pointer :: q.permission :: q.iargs)
 
 
 let add_records_to_map_from_lc = function

lib/explain.ml

@@ -244,9 +244,7 @@ let state (ctxt : C.t) log model_with_q extras =
       | Some (Q ret) ->
         let binder = IT.(Pat (PSym (fst ret.q), snd ret.q, Loc.other __LOC__), None) in
         ITSet.union
-          (ITSet.bigunion_map
-             (subterms_without_bound_variables [])
-             [ ret.pointer; ret.step ])
+          (ITSet.bigunion_map (subterms_without_bound_variables []) [ ret.pointer ])
           (ITSet.bigunion_map
              (subterms_without_bound_variables [ binder ])
              (ret.permission :: ret.iargs))

lib/pack.ml

@@ -29,7 +29,7 @@ let unfolded_array loc init (ict, olength) pointer =
       pointer;
       q = (q_s, Memory.uintptr_bt);
       q_loc = loc;
-      step = IT.uintptr_int_ (Memory.size_of_ctype ict) loc;
+      step = ict;
       iargs = [];
       permission =
         IT.(
@@ -166,15 +166,7 @@ let extractable_one (* global *) prove_or_model (predicate_name, index) (ret, O
        let at_index =
          ( P
              { name = ret.name;
-               pointer =
-                 IT.(
-                   pointer_offset_
-                     ( ret.pointer,
-                       mul_
-                         ( cast_ Memory.uintptr_bt ret.step loc,
-                           cast_ Memory.uintptr_bt index loc )
-                         loc )
-                     loc);
+               pointer = IT.(arrayShift_ ~base:ret.pointer ~index ret.step loc);
                iargs = List.map (IT.subst su) ret.iargs
              },
            O (IT.map_get_ o index loc) )

lib/pp_mucore_coq.ml

@@ -1251,7 +1251,7 @@ and pp_request_qpredicate qpred =
       ("QPredicate.pointer", pp_index_term qpred.pointer);
       ("QPredicate.q", pp_pair pp_symbol (pp_basetype pp_unit) qpred.q);
       ("QPredicate.q_loc", pp_location qpred.q_loc);
-      ("QPredicate.step", pp_index_term qpred.step);
+      ("QPredicate.step", pp_sctype qpred.step);
       ("QPredicate.permission", pp_index_term qpred.permission);
       ("QPredicate.iargs", pp_list pp_index_term qpred.iargs)
     ]

lib/request.ml

@@ -76,23 +76,16 @@ module QPredicate = struct
       pointer : IT.t; (* I *)
       q : Sym.t * BaseTypes.t;
       q_loc : Locations.t; [@equal fun _ _ -> true] [@compare fun _ _ -> 0]
-      step : IT.t;
+      step : Sctypes.ctype;
       permission : IT.t; (* I, function of q *)
       iargs : IT.t list (* I, function of q *)
     }
   [@@deriving eq, ord]
 
   let pp_aux (p : t) oargs =
     let open Pp in
-    (* ISD: this is `p + i * step` but that's "wrong" in a couple of ways:
-       - we are not using the correct precedences for `p` and `step`
-       - in C pointer arithmetic takes account of the types, but here
-         we seem to be doing it at the byte level.  Would `step` ever
-         differ from the size of elements that `p` points to?
-       - perhaps print as `&p[i]` or `&p[j + i]`
-    *)
     let pointer =
-      IT.pp p.pointer ^^^ plus ^^^ Sym.pp (fst p.q) ^^^ star ^^^ IT.pp p.step
+      IT.pp p.pointer ^^^ plus ^^^ Sym.pp (fst p.q) ^^^ at ^^^ Sctypes.pp p.step
     in
     let args = pointer :: List.map IT.pp p.iargs in
     !^"each"
@@ -126,7 +119,7 @@ module QPredicate = struct
       pointer = IT.subst substitution qp.pointer;
       q = qp.q;
       q_loc = qp.q_loc;
-      step = IT.subst substitution qp.step;
+      step = qp.step;
       permission = IT.subst substitution qp.permission;
       iargs = List.map (IT.subst substitution) qp.iargs
     }
@@ -137,7 +130,7 @@ module QPredicate = struct
     Dnode
       ( pp_ctor "qpred",
         Dleaf (Pp.parens (Pp.typ (Sym.pp (fst qpred.q)) (BaseTypes.pp (snd qpred.q))))
-        :: IT.dtree qpred.step
+        :: Dleaf (Sctypes.pp qpred.step)
         :: IT.dtree qpred.permission
         :: dtree_of_name qpred.name
         :: IT.dtree qpred.pointer
@@ -186,15 +179,15 @@ let free_vars_bts = function
       (fun _ bt1 bt2 ->
          assert (BaseTypes.equal bt1 bt2);
          Some bt1)
-      (IT.free_vars_bts_list [ p.pointer; p.step ])
+      (IT.free_vars_bts_list [ p.pointer ])
       (Sym.Map.remove (fst p.q) (IT.free_vars_bts_list (p.permission :: p.iargs)))
 
 
 let free_vars = function
   | P p -> IT.free_vars_list (p.pointer :: p.iargs)
   | Q p ->
     Sym.Set.union
-      (Sym.Set.union (IT.free_vars p.pointer) (IT.free_vars p.step))
+      (IT.free_vars p.pointer)
       (Sym.Set.remove (fst p.q) (IT.free_vars_list (p.permission :: p.iargs)))
 
 
@@ -207,8 +200,6 @@ let alpha_equivalent r1 r2 =
   | _ -> false
 
 
-let steps_constant = function Q qp -> Option.is_some (IT.is_const qp.step) | _ -> true
-
 let dtree = function P pred -> Predicate.dtree pred | Q qpred -> QPredicate.dtree qpred
 
 let get_pointer = function P pred -> pred.pointer | Q qpred -> qpred.pointer

lib/request.mli

@@ -37,7 +37,7 @@ module QPredicate : sig
       pointer : IndexTerms.t;
       q : Sym.t * BaseTypes.t;
       q_loc : Locations.t;
-      step : IndexTerms.t;
+      step : Sctypes.ctype;
       permission : IndexTerms.t;
       iargs : IndexTerms.t list
     }
@@ -83,8 +83,6 @@ val free_vars : t -> Sym.Set.t
 
 val alpha_equivalent : t -> t -> bool
 
-val steps_constant : t -> bool
-
 val dtree : t -> Cerb_frontend.Pp_ast.doc_tree
 
 val get_pointer : t -> IndexTerms.t

lib/resourceInference.ml

@@ -251,33 +251,19 @@ module General = struct
     let@ provable = provable loc in
     let@ simp_ctxt = simp_ctxt () in
     let needed = requested.permission in
-    let step = Simplify.IndexTerms.simp simp_ctxt requested.step in
-    let@ () =
-      if Option.is_some (IT.is_const step) then
-        return ()
-      else (
-        let doc =
-          Pp.(
-            !^"cannot simplify iter-step to constant:"
-            ^^^ IT.pp requested.step
-            ^^ colon
-            ^^^ IT.pp step)
-        in
-        fail (fun _ -> { loc; msg = TypeErrors.Generic doc [@alert "-deprecated"] }))
-    in
+    let step = requested.step in
     let@ (needed, oarg), rw_time =
       map_and_fold_resources
         loc
         (fun re (needed, oarg) ->
            let continue = (Unchanged, (needed, oarg)) in
-           assert (Req.steps_constant (fst re));
            if IT.is_false needed then
              continue
            else (
              match re with
              | Q p', O p'_oarg
                when Req.subsumed requested.name p'.name
-                    && IT.equal step p'.step
+                    && Sctypes.equal step p'.step
                     && BaseTypes.equal (snd requested.q) (snd p'.q) ->
                let p' = Req.QPredicate.alpha_rename_ (fst requested.q) p' in
                let here = Locations.other __LOC__ in
@@ -341,14 +327,7 @@ module General = struct
              | `True ->
                let@ o_re_index =
                  let pointer =
-                   IT.(
-                     pointer_offset_
-                       ( requested.pointer,
-                         mul_
-                           ( cast_ Memory.uintptr_bt requested.step here,
-                             cast_ Memory.uintptr_bt index here )
-                           here ))
-                     here
+                   IT.(arrayShift_ ~base:requested.pointer ~index requested.step here)
                  in
                  predicate_request
                    loc

lib/simplify.ml

@@ -651,7 +651,7 @@ module Request = struct
           pointer = IndexTerms.simp simp_ctxt qp.pointer;
           q = qp.q;
           q_loc = qp.q_loc;
-          step = IndexTerms.simp simp_ctxt qp.step;
+          step = qp.step;
           permission = and_ permission (IT.get_loc qp.permission);
           iargs = List.map (IndexTerms.simp simp_ctxt) qp.iargs
         }

lib/testGeneration/genCompile.ml

@@ -183,7 +183,7 @@ let rec compile_it_lat
       let gt_body =
         let sym_val = Sym.fresh () in
         let it_q = IT.sym_ (q_sym, k_bt, q_loc) in
-        let it_p = IT.add_ (pointer, IT.mul_ (it_q, step) (IT.get_loc step)) loc in
+        let it_p = IT.arrayShift_ ~base:pointer ~index:it_q step loc in
         let gt_asgn =
           GT.asgn_
             ( (it_p, ct),
@@ -218,7 +218,7 @@ let rec compile_it_lat
       let pred = List.assoc Sym.equal fsym preds in
       let arg_syms = pred.pointer :: fst (List.split pred.iargs) in
       let it_q = IT.sym_ (q_sym, q_bt, q_loc) in
-      let it_p = IT.add_ (pointer, IT.mul_ (it_q, step) (IT.get_loc step)) loc in
+      let it_p = IT.arrayShift_ ~base:pointer ~index:it_q step loc in
       let arg_its = it_p :: iargs in
       let args = List.combine arg_syms arg_its in
       (* Build [GT.t] *)

lib/wellTyped.ml

@@ -1111,25 +1111,10 @@ module WReq = struct
       (*normalisation does not change bit types. If this assertion fails, we have to
         adjust the later code to use qbt.*)
       warn_when_not_quantifier_bt "each" loc qbt (Sym.pp (fst p.q));
-      let@ step = WIT.check loc (snd p.q) p.step in
-      let@ step =
-        match step with
-        | IT (Const (Bits (_bits_bt, z)), _, _) ->
-          if Z.lt Z.zero z then
-            return step
-          else
-            fail
-              { loc;
-                msg =
-                  Generic (!^"Iteration step" ^^^ IT.pp p.step ^^^ !^"must be positive")
-                  [@alert "-deprecated"]
-              }
-        | IT (SizeOf _, _, _) -> return step
-        | IT (Cast (_, IT (SizeOf _, _, _)), _, _) -> return step
-        | _ ->
-          let hint = "Only constant iteration steps are allowed." in
-          fail { loc; msg = NIA { it = p.step; hint } }
-      in
+      (* The location is not quite right here (should point to the
+         array_shift<>() itself rather than the pointer) but it's good enough
+         for now. *)
+      let@ () = err_if_ct_void (IT.get_loc p.pointer) `Array_shift p.step in
       let@ permission, iargs =
         pure
           (let@ () = add_l (fst p.q) (snd p.q) (loc, lazy (Pp.string "forall-var")) in
@@ -1153,7 +1138,14 @@ module WReq = struct
       in
       return
         (Req.Q
-           { name = p.name; pointer; q = p.q; q_loc = p.q_loc; step; permission; iargs })
+           { name = p.name;
+             pointer;
+             q = p.q;
+             q_loc = p.q_loc;
+             step = p.step;
+             permission;
+             iargs
+           })
 end
 
 module WRS = struct