From 574805946952028bf9c84fcc79ad2cee13bfc78a Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 1 Apr 2019 09:47:52 +0200
Subject: [PATCH] [WP] casts from/to boolean
---
src/plugins/wp/Cmath.ml | 3 +
src/plugins/wp/Cmath.mli | 3 +
src/plugins/wp/LogicSemantics.ml | 8 +-
.../tests/wp_acsl/oracle/unit_bool.res.oracle | 74 +++++++++++++++
.../oracle_qualif/unit_bool.0.report.json | 93 ++++++++++++++++++-
.../oracle_qualif/unit_bool.res.oracle | 24 ++++-
src/plugins/wp/tests/wp_acsl/unit_bool.i | 21 +++++
7 files changed, 219 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/Cmath.ml b/src/plugins/wp/Cmath.ml
index 73f81d61182..e168c743a9b 100644
--- a/src/plugins/wp/Cmath.ml
+++ b/src/plugins/wp/Cmath.ml
@@ -90,6 +90,9 @@ let builtin_truncate f e =
let int_of_real x = e_fun f_truncate [x]
let real_of_int x = e_fun f_real_of_int [x]
+let int_of_bool a = e_neq a F.e_zero (* if a != 0 then true else false *)
+let bool_of_int a = e_if a F.e_one F.e_zero (* if a then 1 else 0 *)
+
(* -------------------------------------------------------------------------- *)
(* --- Sign --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cmath.mli b/src/plugins/wp/Cmath.mli
index 7c1510ffdc3..c7ba3bd52e4 100644
--- a/src/plugins/wp/Cmath.mli
+++ b/src/plugins/wp/Cmath.mli
@@ -27,6 +27,9 @@
open Lang
open Lang.F
+val int_of_bool : unop
+val bool_of_int : unop
+
val int_of_real : term -> term
val real_of_int : term -> term
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 9deb0c43059..2c8f9c8028b 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -587,7 +587,9 @@ struct
L.map
(fun x -> Cmath.int_of_real (Cfloat.real_of_float f x))
(C.logic env t)
- | L_bool|L_pointer _|L_array _ ->
+ | L_bool ->
+ L.map Cmath.bool_of_int (C.logic env t)
+ | L_pointer _|L_array _ ->
Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
Printer.pp_logic_type src_ltype Printer.pp_logic_type Linteger
@@ -595,7 +597,9 @@ struct
let src_ltype = Logic_utils.unroll_type ~unroll_typedef:false t.term_type in
match cvsort_of_ltype src_ltype with
| L_bool -> C.logic env t
- | L_integer | L_cint _ | L_real | L_cfloat _ | L_pointer _ | L_array _ ->
+ | L_integer | L_cint _ ->
+ L.map Cmath.int_of_bool (C.logic env t)
+ | L_real | L_cfloat _ | L_pointer _ | L_array _ ->
Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
Printer.pp_logic_type src_ltype Printer.pp_logic_type Logic_const.boolean_type
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
index 1cb52118073..d4de7cfa3f0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
@@ -2,6 +2,7 @@
[kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
------------------------------------------------------------
Axiomatic 'Foo'
------------------------------------------------------------
@@ -11,3 +12,76 @@ Assume: 'f_def'
Prove: (L_f 1)
------------------------------------------------------------
+------------------------------------------------------------
+ Function boolean_casts
+------------------------------------------------------------
+
+Goal Check 'C0' (file tests/wp_acsl/unit_bool.i, line 12):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'C1' (file tests/wp_acsl/unit_bool.i, line 13):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'c0' (file tests/wp_acsl/unit_bool.i, line 14):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/unit_bool.i, line 15):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/unit_bool.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'X0' (file tests/wp_acsl/unit_bool.i, line 18):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'X1' (file tests/wp_acsl/unit_bool.i, line 19):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'x0' (file tests/wp_acsl/unit_bool.i, line 20):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'x1' (file tests/wp_acsl/unit_bool.i, line 21):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'x2' (file tests/wp_acsl/unit_bool.i, line 22):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'B0' (file tests/wp_acsl/unit_bool.i, line 24):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'B1' (file tests/wp_acsl/unit_bool.i, line 25):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'b0' (file tests/wp_acsl/unit_bool.i, line 26):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'b1' (file tests/wp_acsl/unit_bool.i, line 27):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
index cce14a76fc5..7ca95e7dd10 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
@@ -1,5 +1,6 @@
{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 1 },
- "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+ "qed": { "total": 14, "valid": 14 },
+ "wp:main": { "total": 15, "valid": 15, "rank": 1 } },
"wp:axiomatics": { "Foo": { "lemma_f_1": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 1 },
@@ -11,4 +12,92 @@
"rank": 1 },
"wp:main": { "total": 1,
"valid": 1,
- "rank": 1 } } } } }
+ "rank": 1 } } } },
+ "wp:functions": { "boolean_casts": { "boolean_casts_check_b1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_b0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_B1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_B0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_x2": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_x1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_x0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_X1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_X0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_c2": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_c1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_c0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_C1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_C0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 14,
+ "valid": 14 },
+ "wp:main": { "total": 14,
+ "valid": 14 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
index 6822d60dd5b..9e87f031a9e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
@@ -2,10 +2,25 @@
[kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
-[wp] 1 goal scheduled
+[wp] Warning: Missing RTE guards
+[wp] 15 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_f_1 : Valid
-[wp] Proved goals: 1 / 1
- Qed: 0
+[wp] [Qed] Goal typed_boolean_casts_check_C0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_C1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_c0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_c1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_c2 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_X0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_X1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_x0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_x1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_x2 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_B0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_B1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_b0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_b1 : Valid
+[wp] Proved goals: 15 / 15
+ Qed: 14
Alt-Ergo: 1
[wp] Report in: 'tests/wp_acsl/oracle_qualif/unit_bool.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/unit_bool.0.report.json'
@@ -13,3 +28,6 @@
Axiomatics WP Alt-Ergo Total Success
Axiomatic Foo - 1 (1..12) 1 100%
-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+boolean_casts 14 - 14 100%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/unit_bool.i b/src/plugins/wp/tests/wp_acsl/unit_bool.i
index 2892c9f8273..dd18aa4f3e0 100644
--- a/src/plugins/wp/tests/wp_acsl/unit_bool.i
+++ b/src/plugins/wp/tests/wp_acsl/unit_bool.i
@@ -6,3 +6,24 @@
lemma f_1: f(1);
}*/
+
+
+_Bool boolean_casts(int x, _Bool y) {
+ //@ check C0: 0 == (integer) \false;
+ //@ check C1: 1 == (integer) \true ;
+ //@ check c0: \false == (boolean) 0;
+ //@ check c1: \true == (boolean) 1;
+ //@ check c2: \true == (boolean) 2;
+ int x0 = 0, x1=1, x2=2;
+ //@ check X0: x0 == (int) \false;
+ //@ check X1: x1 == (int) \true ;
+ //@ check x0: \false == (boolean) x0;
+ //@ check x1: \true == (boolean) x1;
+ //@ check x2: \true == (boolean) x2;
+ _Bool b0=0, b1=1;
+ //@ check B0: b0 == (_Bool) \false;
+ //@ check B1: b1 == (_Bool) \true ;
+ //@ check b0: \false == (boolean) b0;
+ //@ check b1: \true == (boolean) b1;
+ return 0;
+}
--
GitLab