From d03442adb3934904d82fc2bfa7d5eb683f45b5bf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 18 Sep 2019 17:48:56 +0200
Subject: [PATCH] [wp] fix refusage lattice
---
src/plugins/wp/Factory.ml | 36 +++++++++++--------
src/plugins/wp/RefUsage.ml | 15 ++++----
src/plugins/wp/RefUsage.mli | 11 +++---
.../tests/wp_acsl/oracle/pointer.res.oracle | 4 +--
.../oracle_qualif/pointer.0.res.oracle | 2 +-
.../oracle_qualif/pointer.1.res.oracle | 2 +-
.../wp_bts/oracle/issue_715_b.res.oracle | 2 +-
.../oracle_qualif/issue_715_b.0.report.json | 22 ++++++++----
.../d16c9211a53fccb4eb65942166fe02a2.json | 2 ++
.../oracle_qualif/issue_715_b.res.oracle | 10 +++---
.../oracle/reference_array_simple.res.oracle | 2 +-
.../tests/wp_plugin/oracle/dynamic.res.oracle | 4 +--
.../oracle_qualif/dynamic.res.oracle | 4 +--
.../wp_usage/oracle/code_spec.res.oracle | 2 +-
.../wp_usage/oracle/issue-189.1.res.oracle | 3 +-
.../wp_usage/oracle/issue-189.2.res.oracle | 2 +-
16 files changed, 70 insertions(+), 53 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.session/cache/d16c9211a53fccb4eb65942166fe02a2.json
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 23c889c0ac5..f0c8ce79b90 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -172,27 +172,33 @@ end
(* --- RefUsage-based Proxies --- *)
(* -------------------------------------------------------------------------- *)
-let is_formal_ptr x =
- let open Cil_types in
- x.vformal && Cil.isPointerType x.vtype
+let is_ptr x = Cil.isPointerType x.Cil_types.vtype
+let is_fun_ptr x = Cil.isFunctionType x.Cil_types.vtype
+let is_formal_ptr x = x.Cil_types.vformal && is_ptr x
+let is_init kf x =
+ WpStrategy.is_main_init kf ||
+ Wp_parameters.AliasInit.get () ||
+ ( WpStrategy.isInitConst () && WpStrategy.isGlobalInitConst x )
let refusage_param ~byref ~context x =
let kf,init = match WpContext.get_scope () with
- | WpContext.Global -> None,false
- | WpContext.Kf f ->
- Some f ,
- WpStrategy.is_main_init f ||
- Wp_parameters.AliasInit.get () ||
- ( WpStrategy.isInitConst () &&
- WpStrategy.isGlobalInitConst x ) in
+ | WpContext.Global -> None , false
+ | WpContext.Kf kf -> Some kf , is_init kf x in
match RefUsage.get ?kf ~init x with
| RefUsage.NoAccess -> MemoryContext.NotUsed
| RefUsage.ByAddr -> MemoryContext.ByAddr
- | RefUsage.ByRef when byref -> MemoryContext.ByRef
- | RefUsage.ByArray when context && is_formal_ptr x -> MemoryContext.InArray
- | RefUsage.ByValue when context && is_formal_ptr x -> MemoryContext.InContext
- | RefUsage.ByRef | RefUsage.ByValue -> MemoryContext.ByValue
- | RefUsage.ByArray -> MemoryContext.ByShift
+ | RefUsage.ByValue ->
+ if context && is_formal_ptr x then MemoryContext.InContext
+ else if is_ptr x && not (is_fun_ptr x) then MemoryContext.ByShift
+ else MemoryContext.ByValue
+ | RefUsage.ByRef ->
+ if byref
+ then MemoryContext.ByRef
+ else MemoryContext.ByValue
+ | RefUsage.ByArray ->
+ if context && is_formal_ptr x
+ then MemoryContext.InArray
+ else MemoryContext.ByShift
let refusage_iter ?kf ~init f = RefUsage.iter ?kf ~init (fun x _usage -> f x)
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 38647c7e307..0d8e62d907c 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -32,12 +32,13 @@ open Cil_datatype
(* --- Varinfo Accesses --- *)
(* ---------------------------------------------------------------------- *)
+(** By lattice order of usage *)
type access =
- | NoAccess
- | ByRef (* The expr ["*x"], equals to [load(load(&x))] *)
- | ByArray (* The expr ["x[_]"], equals to [load(shift(load(&x),_))] *)
- | ByValue (* The expr ["x"], equals to [load(&x)] *)
- | ByAddr (* The expr ["&x"] *)
+ | NoAccess (** Never used *)
+ | ByRef (** Only used as ["*x"], equals to [load(shift(load(&x),0))] *)
+ | ByArray (** Only used as ["x[_]"], equals to [load(shift(load(&x),_))] *)
+ | ByValue (** Only used as ["x"], equals to [load(&x)] *)
+ | ByAddr (** Widely used, potentially up to ["&x"] *)
module Access :
sig
@@ -59,8 +60,8 @@ struct
let rank = function
| NoAccess -> 0
| ByRef -> 1
- | ByValue -> 2
- | ByArray -> 3
+ | ByArray -> 2
+ | ByValue -> 3
| ByAddr -> 4
let cup a b = if rank a < rank b then b else a
diff --git a/src/plugins/wp/RefUsage.mli b/src/plugins/wp/RefUsage.mli
index 7a50bebcd53..ca3e2cf74ef 100644
--- a/src/plugins/wp/RefUsage.mli
+++ b/src/plugins/wp/RefUsage.mli
@@ -26,12 +26,13 @@
open Cil_types
+(** By lattice order of usage *)
type access =
- | NoAccess
- | ByRef (* The expression ["*x"], equal to [load(load(&x))] *)
- | ByArray (* The expression ["x[_]"], equal to [load(shift(load(&x),_))] *)
- | ByValue (* The expression ["x"], equal to [load(&x)] *)
- | ByAddr (* The expression ["&x"] *)
+ | NoAccess (** Never used *)
+ | ByRef (** Only used as ["*x"], equals to [load(shift(load(&x),0))] *)
+ | ByArray (** Only used as ["x[_]"], equals to [load(shift(load(&x),_))] *)
+ | ByValue (** Only used as ["x"], equals to [load(&x)] *)
+ | ByAddr (** Widely used, potentially up to ["&x"] *)
val get : ?kf:kernel_function -> ?init:bool -> varinfo -> access
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
index e428c32c2f5..ee7c5d3d75a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
@@ -270,8 +270,8 @@ Prove: false.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'compare':
- /*@ behavior typed: requires \separated(&p,q); */
+ /*@ behavior typed: requires \separated(&p,q+(..)); */
void compare(int *q);
[wp] Warning: Memory model hypotheses for function 'absurd':
- /*@ behavior typed: requires \separated(&p,q); */
+ /*@ behavior typed: requires \separated(&p,q+(..)); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
index 3638dce1955..1ef1281118e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
@@ -28,5 +28,5 @@ mixed_array_pointer - - 2 0.0%
absurd - - 2 0.0%
-------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'absurd':
- /*@ behavior typed_ref: requires \separated(&p,q); */
+ /*@ behavior typed_ref: requires \separated(&p,q+(..)); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
index 9d969ebd5f4..3e8203adc10 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
@@ -28,5 +28,5 @@ mixed_array_pointer - - 2 0.0%
absurd - - 2 0.0%
-------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'absurd':
- /*@ behavior typed: requires \separated(&p,q); */
+ /*@ behavior typed: requires \separated(&p,q+(..)); */
void absurd(int *q);
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
index 13a226ffae8..a786d13c966 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
@@ -12,7 +12,7 @@
Goal Instance of 'Pre-condition (file tests/wp_bts/issue_715_b.i, line 4) in 'dummy'' in 'foo' at call 'dummy' (file tests/wp_bts/issue_715_b.i, line 11)
:
Assume { (* Heap *) Have: linked(Malloc_0). }
-Prove: P_isValid(Malloc_0, shift_sint32(global(L_p_28), 0)).
+Prove: P_isValid(Malloc_0[L_p_28 <- 1], shift_sint32(global(L_p_28), 0)).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.report.json
index 9cdd29b8d19..f700fbcb428 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.report.json
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.report.json
@@ -1,13 +1,21 @@
-{ "wp:global": { "qed": { "total": 1, "valid": 1 },
- "wp:main": { "total": 2, "valid": 1, "unknown": 1 } },
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 3 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 2, "rank": 3 } },
"wp:functions": { "foo": { "dummy_requires_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
- "dummy_requires": { "wp:main": { "total": 1,
- "unknown": 1 } },
- "wp:section": { "qed": { "total": 1,
+ "dummy_requires": { "why3:Alt-Ergo,2.0.0":
+ { "total": 1, "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 2,
- "valid": 1,
- "unknown": 1 } } } } }
+ "valid": 2,
+ "rank": 3 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.session/cache/d16c9211a53fccb4eb65942166fe02a2.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.session/cache/d16c9211a53fccb4eb65942166fe02a2.json
new file mode 100644
index 00000000000..5607410e7fd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.0.session/cache/d16c9211a53fccb4eb65942166fe02a2.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0189,
+ "steps": 13 }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
index fbb80ae85bd..240b17af9df 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
@@ -6,14 +6,14 @@
No code nor implicit assigns clause for function dummy, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] Warning: creating session directory `tests/wp_bts/oracle_qualif/issue_715_b.0.session'
-[wp] [Failed] Goal typed_foo_call_dummy_requires
+[wp] [Alt-Ergo 2.0.0] Goal typed_foo_call_dummy_requires : Valid
[wp] [Qed] Goal typed_foo_call_dummy_requires_2 : Valid
-[wp] Proved goals: 1 / 2
- Qed: 1
+[wp] Proved goals: 2 / 2
+ Qed: 1
+ Alt-Ergo 2.0.0: 1
[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_715_b.0.report.json'
[wp] Report out: 'tests/wp_bts/result_qualif/issue_715_b.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-foo 1 - 2 50.0%
+foo 1 1 (8..20) 2 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
index 90e29f22ce3..e71891e1ea8 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_array_simple.res.oracle
@@ -8,7 +8,7 @@ Init: { }
Function f1: { p1[] i }
Function call_f1: { tt tmp }
Function f2: { p2[] j }
-Function call_f2: { tt tmp[] __retres }
+Function call_f2: { tt tmp __retres }
Function f3: { p3[] k }
Function call_f3: { tp tmp }
.................................................
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index cd88f4ec2a0..c2bc3a37416 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -377,10 +377,10 @@ Prove: true.
/*@ behavior typed: requires \separated(&X,p); */
void guarded_call(struct S *p);
[wp] Warning: Memory model hypotheses for function 'behavior':
- /*@ behavior typed: requires \separated(&X1,p); */
+ /*@ behavior typed: requires \separated(&X1,p+(..)); */
int behavior(int (*p)(void));
[wp] Warning: Memory model hypotheses for function 'some_behaviors':
- /*@ behavior typed: requires \separated(&X1,p); */
+ /*@ behavior typed: requires \separated(&X1,p+(..)); */
int some_behaviors(int (*p)(void));
[wp] Warning: Memory model hypotheses for function 'missing_context':
/*@ behavior typed: requires \separated(&X1,p); */
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index 7fdb8a52676..b7dfadf11d6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -74,10 +74,10 @@ no_call 4 - 4 100%
/*@ behavior typed: requires \separated(&X,p); */
void guarded_call(struct S *p);
[wp] Warning: Memory model hypotheses for function 'behavior':
- /*@ behavior typed: requires \separated(&X1,p); */
+ /*@ behavior typed: requires \separated(&X1,p+(..)); */
int behavior(int (*p)(void));
[wp] Warning: Memory model hypotheses for function 'some_behaviors':
- /*@ behavior typed: requires \separated(&X1,p); */
+ /*@ behavior typed: requires \separated(&X1,p+(..)); */
int some_behaviors(int (*p)(void));
[wp] Warning: Memory model hypotheses for function 'missing_context':
/*@ behavior typed: requires \separated(&X1,p); */
diff --git a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
index e4ad3f5e78b..a812acef1d1 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
@@ -37,7 +37,7 @@ Function calling_spec:
val_val3 val_ref1 *ref_ref2 array_ref3[] v1 v2 v3 v4 val_array1
array_array2[] array_array3[] }
Function cup:
-{ val *ref &addr array[] &addr_value val_ref array_ref[] value_array[] }
+{ val *ref &addr array[] &addr_value val_ref array_ref[] value_array }
.................................................
[wp] Loading driver 'share/wp.driver'
[wp] [CFG] Goal by_addr_in_code_annotation_requires : Valid (Unreachable)
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle
index 5bdfc472717..5e33a1a8de1 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.1.res.oracle
@@ -5,11 +5,10 @@
... Ref Usage
.................................................
Init: { }
-Function f: { *ptr src[] idx }
+Function f: { *ptr src idx }
.................................................
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] tests/wp_usage/issue-189.i:18: Warning: Undefined array-size (sint8[])
[wp] tests/wp_usage/issue-189.i:17: Warning:
forbidden write to variable 'src' considered in an isolated context.
Use model 'Typed' instead or specify '-wp-unalias-vars src'
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
index efc2cf67736..ec41c7f550d 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
@@ -5,7 +5,7 @@
... Ref Usage
.................................................
Init: { }
-Function f: { *ptr src[] idx }
+Function f: { *ptr src idx }
.................................................
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
--
GitLab