[Builtin] Smarter management of sizeof

src/plugins/builtin/basic_blocks.ml

@@ -150,20 +150,20 @@ let taccess ?loc ptr offset =
     term ?loc (TLval lval) (ttype_of_pointed ptr.term_type)
   | _ -> assert false
 
-let tsizeofpointed ?loc = function
-  | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> tinteger ?loc (Cil.bytesSizeOf t)
+let sizeofpointed = function
+  | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Cil.bytesSizeOf t
   | _ -> assert false
 
-let tlen_div_size ?loc t bytes_len =
-  let sizeof = tsizeofpointed ?loc t in
-  tdivide ?loc bytes_len sizeof
-
 (** Features related to predicates *)
 
 let plet_len_div_size ?loc t bytes_len pred =
-  let len = tlen_div_size t bytes_len in
-  let len_var = size_var Linteger len in
-  plet ?loc len_var (pred (tvar len_var.l_var_info))
+  let sizeof = sizeofpointed t in
+  if sizeof = 1 then
+    pred bytes_len
+  else
+    let len = tdivide ?loc bytes_len (tinteger ?loc sizeof) in
+    let len_var = size_var Linteger len in
+    plet ?loc len_var (pred (tvar len_var.l_var_info))
 
 let pgeneric_valid_buffer ?loc validity lbl ptr len =
   let buffer = tbuffer_range ?loc ptr len in
@@ -176,11 +176,11 @@ let pvalid_len_bytes ?loc = pgeneric_valid_len_bytes ?loc pvalid
 let pvalid_read_len_bytes ?loc = pgeneric_valid_len_bytes ?loc pvalid_read
 
 let pcorrect_len_bytes ?loc t bytes_len =
-  let sizeof = tsizeofpointed ?loc t in
+  let sizeof = tinteger ?loc (sizeofpointed t) in
   let modulo = term ?loc (TBinOp(Mod, bytes_len, sizeof)) Linteger in
   prel ?loc (Req, modulo, tinteger ?loc 0)
 
-let pindex_bounds ?loc low value up =
+let pbounds_incl_excl ?loc low value up =
   let geq_0 = prel ?loc (Rle, low, value) in
   let lt_len = prel ?loc (Rlt, value, up) in
   pand ?loc (geq_0, lt_len)
@@ -191,7 +191,7 @@ let rec punfold_all_elems_eq ?loc t1 t2 len =
 and pall_elems_eq ?loc depth t1 t2 len =
   let ind = Cil_const.make_logic_var_quant ("j" ^ (string_of_int depth)) Linteger in
   let tind = tvar ind in
-  let bounds = pindex_bounds ?loc (tinteger 0) tind len in
+  let bounds = pbounds_incl_excl ?loc (tinteger 0) tind len in
   let t1_acc = taccess ?loc t1 tind in
   let t2_acc = taccess ?loc t2 tind in
   let eq = peq_unfold ?loc (depth+1) t1_acc t2_acc in
@@ -203,6 +203,22 @@ and peq_unfold ?loc depth t1 t2 =
     pall_elems_eq ?loc depth t1 t2 len
   | _ -> prel ?loc (Req, t1, t2)
 
+let rec punfold_all_elems_eq_val ?loc t1 value len =
+  pall_elems_eq ?loc 0 t1 value len
+and pall_elems_eq ?loc depth t1 value len =
+  let ind = Cil_const.make_logic_var_quant ("j" ^ (string_of_int depth)) Linteger in
+  let tind = tvar ind in
+  let bounds = pbounds_incl_excl ?loc (tinteger 0) tind len in
+  let t1_acc = taccess ?loc t1 tind in
+  let eq = peq_unfold ?loc (depth+1) t1_acc value in
+  pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
+and peq_unfold ?loc depth t1 value =
+  match t1.term_type with
+  | Ctype(TArray(_, Some len, _, _)) ->
+    let len = Logic_utils.expr_to_term ~cast:false len in
+    pall_elems_eq ?loc depth t1 value len
+  | _ -> prel ?loc (Req, t1, value)
+
 let pseparated_memories ?loc p1 len1 p2 len2 =
   let b1 = tbuffer_range ?loc p1 len1 in
   let b2 = tbuffer_range ?loc p2 len2 in

src/plugins/builtin/basic_blocks.mli

@@ -40,10 +40,12 @@ val tplus: ?loc:location -> term -> term -> term
 val tminus: ?loc:location -> term -> term -> term
 val tdivide: ?loc:location -> term -> term -> term
 
+val pbounds_incl_excl: ?loc:location -> term -> term -> term -> predicate
 val pvalid_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
 val pvalid_read_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
 val pcorrect_len_bytes: ?loc:location -> logic_type -> term -> predicate
 val punfold_all_elems_eq: ?loc:location -> term -> term -> term -> predicate
+val punfold_all_elems_eq_val: ?loc:location -> term -> term -> term -> predicate
 
 val pseparated_memories: ?loc:location -> term -> term -> term -> term -> predicate