From b8c2f7ed1d5a7528e9488e02039f83d1bbd8a72e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 22 Sep 2020 15:23:32 +0200
Subject: [PATCH] [wp] Introduces table abstract type for offsets
---
src/plugins/wp/MemMemory.ml | 15 +++++++++------
src/plugins/wp/share/coqwp/Memory.v | 13 ++++++++-----
src/plugins/wp/share/why3/frama_c_wp/memory.mlw | 16 +++++++++-------
.../tests/wp_acsl/oracle/base_offset.res.oracle | 10 +++++-----
.../init_t2_bis_v2_assigns_exit_part2.json | 4 ++--
.../init_t2_bis_v2_assigns_normal_part2.json | 4 ++--
.../init_t2_bis_v2_loop_assigns_part2.json | 4 ++--
.../init_t2_bis_v2_loop_assigns_part3.json | 4 ++--
8 files changed, 39 insertions(+), 31 deletions(-)
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index c010c839074..c0f4455e346 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -47,11 +47,14 @@ let f_shift = Lang.extern_f ~library ~result:t_addr "shift"
let f_global = Lang.extern_f ~library ~result:t_addr ~category:L.Injection "global"
let f_null = Lang.extern_f ~library ~result:t_addr "null"
-let f_base_offset_table = Lang.extern_f ~library
- ~category:Qed.Logic.Function ~result:L.Int "base_offset_table"
+let a_table = Lang.datatype ~library "table"
+let t_table = L.Data(a_table,[])
-let f_base_offset = Lang.extern_f ~library
- ~category:Qed.Logic.Injection ~result:L.Int "base_offset"
+let f_table_of_base = Lang.extern_f ~library
+ ~category:Qed.Logic.Function ~result:t_table "table_of_base"
+
+let f_table_to_offset = Lang.extern_f ~library
+ ~category:Qed.Logic.Injection ~result:L.Int "table_to_offset"
let ty_fst_arg = function
| Some l :: _ -> l
@@ -112,8 +115,8 @@ let a_global b = e_fun f_global [b]
let a_shift l k = e_fun f_shift [l;k]
let a_addr b k = a_shift (a_global b) k
let a_base_offset b k =
- let offset_index = e_fun f_base_offset_table [b] in
- e_fun f_base_offset [offset_index ; k]
+ let offset_index = e_fun f_table_of_base [b] in
+ e_fun f_table_to_offset [offset_index ; k]
(* -------------------------------------------------------------------------- *)
(* --- Qed Simplifiers --- *)
diff --git a/src/plugins/wp/share/coqwp/Memory.v b/src/plugins/wp/share/coqwp/Memory.v
index 05f7eaacdd2..ff59f9557f9 100644
--- a/src/plugins/wp/share/coqwp/Memory.v
+++ b/src/plugins/wp/share/coqwp/Memory.v
@@ -347,12 +347,15 @@ Admitted.
Definition addr_of_int : Z -> addr.
Admitted.
+Definition table : Type.
+Admitted.
+
(* Why3 goal *)
-Definition base_offset: Z -> Z -> Z.
+Definition table_to_offset: table -> Z -> Z.
Admitted.
(* Why3 goal *)
-Definition base_offset_table: Z -> Z.
+Definition table_of_base: Z -> table.
Admitted.
(* Why3 goal *)
@@ -370,12 +373,12 @@ Lemma addr_of_null : ((int_of_addr null) = 0%Z).
Admitted.
(* Why3 goal *)
-Lemma base_offset_zero : forall (t: Z), ((base_offset t 0%Z) = 0%Z).
+Lemma table_to_offset_zero : forall (t: table), ((table_to_offset t 0%Z) = 0%Z).
Admitted.
(* Why3 goal *)
-Lemma base_offset_monotonic : forall (t:Z) (i:Z) (j:Z), (i <= j)%Z ->
- ((base_offset t i) <= (base_offset t j))%Z.
+Lemma table_to_offset_monotonic : forall (t:table) (i:Z) (j:Z), (i <= j)%Z ->
+ ((table_to_offset t i) <= (table_to_offset t j))%Z.
Admitted.
Definition cinits (m: farray addr bool) : Prop.
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index fffb52d4ea1..c2f0cc8634b 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -182,15 +182,17 @@ theory Memory
function int_of_addr addr : int
function addr_of_int int : addr
- function base_offset int int : int
- function base_offset_table int : int
- axiom base_offset_zero:
- forall table: int. base_offset table 0 = 0
+ type table (* abstract for now, but can be more elaborated later on *)
+ function table_of_base int : table
+ function table_to_offset table int : int
- axiom base_offset_monotonic:
- forall table o1 o2: int.
- o1 <= o2 <-> base_offset table o1 <= base_offset table o2
+ axiom table_to_offset_zero:
+ forall t: table. table_to_offset t 0 = 0
+
+ axiom table_to_offset_monotonic:
+ forall t: table. forall o1 o2: int.
+ o1 <= o2 <-> table_to_offset t o1 <= table_to_offset t o2
axiom int_of_addr_bijection :
forall a:int. int_of_addr (addr_of_int a) = a
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
index 3876073ea1f..386eb1ab4c2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
@@ -18,15 +18,15 @@ Prove: true.
Goal Post-condition (file tests/wp_acsl/base_offset.i, line 15) in 'f':
Let x = p.base.
-Let x_1 = base_offset_table(x).
-Let x_2 = p.offset.
+Let a = table_of_base(x).
+Let x_1 = p.offset.
Assume {
(* Heap *)
Type: region(x) <= 0.
(* Goal *)
When: (0 <= i) /\ (i <= i_1) /\ (i_1 <= 3).
}
-Prove: base_offset(x_1, 1 + i + x_2) <= base_offset(x_1, 1 + i_1 + x_2).
+Prove: table_to_offset(a, 1 + i + x_1) <= table_to_offset(a, 1 + i_1 + x_1).
------------------------------------------------------------
------------------------------------------------------------
@@ -34,11 +34,11 @@ Prove: base_offset(x_1, 1 + i + x_2) <= base_offset(x_1, 1 + i_1 + x_2).
------------------------------------------------------------
Goal Check 'KO' (file tests/wp_acsl/base_offset.i, line 29):
-Prove: base_offset_table(G_z_33) = base_offset_table(G_x_31).
+Prove: table_of_base(G_z_33) = table_of_base(G_x_31).
------------------------------------------------------------
Goal Check 'KO' (file tests/wp_acsl/base_offset.i, line 30):
-Prove: base_offset_table(G_y_32) != base_offset_table(G_x_31).
+Prove: table_of_base(G_y_32) != table_of_base(G_x_31).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index 2b58bbe6577..3a1b937b6ff 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0092,
+ "verdict": "valid", "time": 0.0097,
"steps": 12 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0095,
+ "verdict": "valid", "time": 0.0109,
"steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index 2b58bbe6577..3a1b937b6ff 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0092,
+ "verdict": "valid", "time": 0.0097,
"steps": 12 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0095,
+ "verdict": "valid", "time": 0.0109,
"steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index be4d92c4fe5..d177a98c28b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0106,
+ "verdict": "valid", "time": 0.0124,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0128,
+ "verdict": "valid", "time": 0.009,
"steps": 28 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index b790982cc65..f5c72396b7f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0097,
+ "verdict": "valid", "time": 0.0133,
"steps": 16 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0105,
+ "verdict": "valid", "time": 0.0081,
"steps": 22 } ] } } ]
--
GitLab