From fcf35a4c86dcceb8e3150aa7526cc7caf3c538a8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 21 Jan 2021 14:24:53 +0100
Subject: [PATCH] [wp] Extend -wp-unfold-assigns to handle ranges
---
src/plugins/wp/LogicSemantics.ml | 81 ++++++++++++++++++-
src/plugins/wp/Sigs.ml | 3 +-
src/plugins/wp/cfgWP.ml | 3 +-
.../oracle/unfold_assigns.0.res.oracle | 41 ++++++++++
.../oracle/unfold_assigns.1.res.oracle | 37 +++++++++
.../wp/tests/wp_plugin/unfold_assigns.i | 9 +++
6 files changed, 168 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 682e9adb223..f2bbd01805f 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -1082,12 +1082,85 @@ struct
(* --- CheckAssigns --- *)
(* -------------------------------------------------------------------------- *)
- let check_assigns sigma ~written ~assignable =
+ let rec decompose_region (obj, sloc) =
+ let is_primitive_int t = Lang.F.is_int t && Lang.F.is_primitive t in
+ match sloc with
+ | Sloc loc ->
+ begin match obj with
+ | C_pointer _ | C_int _ | C_float _
+ | C_comp { cfields = None } | C_array { arr_flat = None } ->
+ [obj, sloc]
+
+ | C_comp { cfields = Some fields } ->
+ let slocs_of_field f =
+ let obj = Ctypes.object_of f.ftype in
+ decompose_region (obj, (Sloc (M.field loc f)))
+ in
+ List.(concat (map slocs_of_field fields))
+
+ | C_array { arr_flat = Some { arr_size=len ; arr_cell=typ } } ->
+ let obj = Ctypes.object_of typ in
+ decompose_range loc obj Z.zero (Z.of_int (len - 1))
+ end
+
+ | Sarray (loc, obj, n) ->
+ decompose_range loc obj Z.zero (Z.of_int (n - 1))
+
+ | Srange (loc, obj, Some b, Some e)
+ when is_primitive_int b && is_primitive_int e ->
+ let b, e = match Lang.F.repr b, Lang.F.repr e with
+ | Kint b, Kint e -> b, e
+ | _ -> assert false (* by match guard *)
+ in
+ decompose_range loc obj b e
+
+ | _ ->
+ (* It is not trivial to go further: the list of regions depends on some
+ unknown values (length of the range, property, ...) *)
+ [obj, sloc]
+
+ and decompose_range l obj b e =
+ let rec generate_i l f i =
+ if Z.leq i b then l
+ else generate_i (f i :: l) f (Z.sub i Z.one)
+ in
+ let slocs_of_index i =
+ let l = M.shift l obj (e_zint i) in
+ decompose_region (obj, (Sloc l))
+ in
+ List.(concat (generate_i [] slocs_of_index e))
+
+ let rec assignable_region ~unfold reg assignable =
+ let check_inclusion reg =
+ p_any (L.included reg) assignable
+ in
+ if unfold then
+ (* This phase unfolds terms that cannot be "statically" unfolded *)
+ let logic_decompose = function
+ | (_, Sloc _) as s -> check_inclusion s
+ | (_, Sarray _) -> assert false (* decompose always remove Sarray *)
+ | (obj, Sdescr(xs, l, p)) ->
+ let sloc = obj, Sloc l in
+ p_forall xs
+ (p_imply p (assignable_region ~unfold:true sloc assignable))
+ | (_, Srange(l, obj, low, up)) ->
+ let x = Lang.freshvar ~basename:"k" Lang.t_int in
+ let k = e_var x in
+ let p = Vset.in_range k low up in
+ let sloc = obj, Sloc (M.shift l obj k) in
+ p_forall [x]
+ (p_imply p (assignable_region ~unfold:true sloc assignable))
+ in
+ p_all logic_decompose (decompose_region reg)
+ else
+ check_inclusion reg
+
+ let check_assigns ~unfold sigma ~written ~assignable =
p_all
- (fun seg ->
+ (fun reg ->
p_imply
- (p_not (L.invalid sigma seg))
- (p_any (L.included seg) assignable)
+ (p_not (L.invalid sigma reg))
+ (assignable_region ~unfold reg assignable)
) (written : region)
end
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 1b594803754..7973ef55de1 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -812,7 +812,8 @@ sig
Compute a formula that checks whether written locations are either
invalid (at the given memory location)
or included in some assignable region. *)
- val check_assigns : sigma -> written:region -> assignable:region -> pred
+ val check_assigns :
+ unfold:bool -> sigma -> written:region -> assignable:region -> pred
end
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index ebf53f21db4..4c8d46d3d00 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -517,7 +517,8 @@ struct
(* -------------------------------------------------------------------------- *)
let assigns_condition (region : L.region) (e:effect) : F.pred =
- L.check_assigns e.e_valid ~written:region ~assignable:e.e_region
+ let unfold = Wp_parameters.UnfoldAssigns.get () in
+ L.check_assigns ~unfold e.e_valid ~written:region ~assignable:e.e_region
exception COLLECTED
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
index 60291308af6..8178bf2d553 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.0.res.oracle
@@ -97,6 +97,47 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 28) in 'NO_UNFOLD_OK_3
Call Effect at line 30
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function PARTIAL_ASSIGNS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
+Call Effect at line 74
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Assume {
+ Have: 0 <= n.
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, x).
+ (* Pre-condition *)
+ Have: 5 <= n.
+}
+Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
+ included(a, x, shift_sint32(p, n), 1).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
+Call Effect at line 74
+Let a = shift_sint32(p, 0).
+Let x = 1 + n.
+Assume {
+ Have: 0 <= n.
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, x).
+ (* Pre-condition *)
+ Have: 5 <= n.
+}
+Prove: (n <= 0) \/ included(a, x, shift_sint32(p, 1), n - 1) \/
+ included(a, x, shift_sint32(p, n), 1).
+
------------------------------------------------------------
------------------------------------------------------------
Function USE_ASSIGN_UNFOLD_KO
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
index f681ec0f923..cb15fe7af3f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unfold_assigns.1.res.oracle
@@ -79,6 +79,43 @@ Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 28) in 'NO_UNFOLD_OK_3
Call Effect at line 30
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function PARTIAL_ASSIGNS
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
+Call Effect at line 74
+Assume {
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= n) /\
+ (!invalid(Malloc_0, shift_sint32(p, 0), 1 + n)).
+ (* Pre-condition *)
+ Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/
+ included(shift_sint32(p, i), 1, shift_sint32(p, 1), n - 1).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/unfold_assigns.i, line 72) in 'PARTIAL_ASSIGNS':
+Call Effect at line 74
+Assume {
+ Type: is_uint32(n).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= n) /\
+ (!invalid(Malloc_0, shift_sint32(p, 0), 1 + n)).
+ (* Pre-condition *)
+ Have: 5 <= n.
+}
+Prove: (i = 0) \/ (n = i) \/
+ included(shift_sint32(p, i), 1, shift_sint32(p, 1), n - 1).
+
------------------------------------------------------------
------------------------------------------------------------
Function USE_ASSIGN_UNFOLD_KO
diff --git a/src/plugins/wp/tests/wp_plugin/unfold_assigns.i b/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
index 54ba848675c..24c9a9347bd 100644
--- a/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
+++ b/src/plugins/wp/tests/wp_plugin/unfold_assigns.i
@@ -64,3 +64,12 @@ void ASSIGN_NO_UNFOLD_KO(struct S *s) {
struct S p = { 0,1 };
*s = p ;
}
+
+/*@ assigns *(p+(0..n)); */
+void f_assigns_array(int *p, unsigned n);
+
+/*@ requires n > 4 ;
+ assigns *(p+0), *(p+(1..n-1)), *(p+n); */
+void PARTIAL_ASSIGNS(int *p, unsigned n) {
+ f_assigns_array(p, n);
+}
--
GitLab