diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 4e5934aecd7ab1aea3c6254f8b40793c8159f9c6..7003dcb3557536e46ec4500519fe2700ebe83c8d 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -915,6 +915,7 @@ module N = struct
let ( >= ) x y = p_leq y x
let ( <> ) = p_neq
+ let ( ==> ) = p_imply
let ( && ) = p_and
let ( || ) = p_or
let not = p_not
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index d712813651f3837d6abaa02872976305425a8189..d2c06c5839ab1b92ca83851017b3a28ca8f12d71 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -520,6 +520,7 @@ module N: sig
val ( >= ): F.cmp (** {! F.p_leq } with inversed argument *)
val ( <> ): F.cmp (** {! F.p_neq } *)
+ val ( ==> ): F.operator (** {! F.p_imply } *)
val ( && ): F.operator (** {! F.p_and } *)
val ( || ): F.operator (** {! F.p_or } *)
val not: F.pred -> F.pred (** {! F.p_not } *)
diff --git a/src/plugins/wp/TacOverflow.ml b/src/plugins/wp/TacOverflow.ml
index 906c596c61a6bbe0842c4cf62473eb99854bf550..406c1101709d2e92c2e4df2b43d40f18341581c8 100644
--- a/src/plugins/wp/TacOverflow.ml
+++ b/src/plugins/wp/TacOverflow.ml
@@ -28,7 +28,7 @@ class overflow =
inherit Tactical.make
~id:"Wp.overflow"
~title:"Overflow"
- ~descr:"Consider no overflow nor downcast"
+ ~descr:"Split integer overflow into in and out of range"
~params:[]
method select _feedback selection =
@@ -36,20 +36,26 @@ class overflow =
let open Qed.Logic in
match F.repr e with
| Fun(f,[v]) ->
- let iota = Cint.to_cint f in
- let cond = Cint.range iota v in
- (*
- let a,b = Ctypes.bounds iota in
- let range = F.p_and
- (F.p_leq (F.e_zint a) v)
- (F.p_leq v (F.e_zint b)) in
- *)
- Applicable( fun (hs,g) -> [
- "In-Range", (hs , cond) ;
- "No-Overflow" ,
- Conditions.subst
- (fun u -> if u == e then v else raise Not_found)
- (hs , F.p_imply cond g)
+ let open Lang.F in
+ let open Lang.N in
+ let min, max = Ctypes.bounds @@ Cint.to_cint f in
+ let min, max = e_zint min, e_zint max in
+
+ let lower = v < min and upper = max < v in
+ let in_range = not (lower || upper) in
+
+ let length = (max - min) + e_one in
+ let overflow = min + ((v - min) mod length) in
+
+ let replace_with v = fun u -> if u == e then v else raise Not_found in
+
+ Applicable(fun (hs,g) -> [
+ "In-Range",
+ Conditions.subst (replace_with v) (hs , in_range ==> g) ;
+ "Lower",
+ Conditions.subst (replace_with overflow) (hs , lower ==> g) ;
+ "Upper",
+ Conditions.subst (replace_with overflow) (hs , upper ==> g)
])
| _ -> Not_applicable
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 950ec5f52dee7cb2a9879b5c730a703f879d6fa0..d3bfd7913e65cb3273a9ce54a2a4489765c5dcd7 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -487,19 +487,25 @@ $G(n) \equiv P(n)\Longrightarrow\,Q(n)$:
\end{array}} \]
\paragraph{Overflow} Integer Conversions \\
-This tactic rewrites machine integer conversions by identity,
-providing the converted value is in available range. The tactic applies on expression
-with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer name,
-\emph{eg.} \texttt{to\_uint32}.
+This tactic split machine integer conversions into three cases: value in integer
+range, lower than range and upper than range. The tactic applies on expression
+with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer
+name, \emph{eg.} \texttt{to\_uint32}.
\[\TACTIC{\Delta\models G}{%
\begin{array}[t]{rcl}
-\Delta\phantom{)} &\models & a \leq e \leq b \\
-\sigma(\Delta) & \models & \sigma(G)
+\sigma_{id}(\Delta) & \models & low \leq e \leq up \Rightarrow \sigma_{id}(G) \\
+\sigma_{+}(\Delta) & \models & low < e \Rightarrow \sigma_{+}(G) \\
+\sigma_{-}(\Delta) & \models & e < up \Rightarrow \sigma_{-}(G)
\end{array}
}\]
-where $\sigma = [ \mathtt{to\_iota}(e) \mapsto e ]$ and $[a..b]$ is the range
-of the \texttt{iota} integer domain.
+where
+\begin{itemize}
+ \item $[low..up]$ is the range of the \texttt{iota} integer domain,
+ \item $\sigma_{id} = [ \mathtt{to\_iota}(e) \mapsto e ]$,
+ \item $\sigma_{+} = [ \mathtt{to\_iota}(e) \mapsto \mathtt{overflow}(e) ]$,
+ \item $\sigma_{-} = [ \mathtt{to\_iota}(e) \mapsto \mathtt{overflow}(e) ]$.
+\end{itemize}
\paragraph{Range} Enumerate a range of values for an integer term\\
The user select any integer expression $e$ in the proof, and a range of numerical values $a\ldots b$. The proof goes by case for each $e=a\ldots e=b$, plus the side cases $e<a$ and $e>b$:
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
index da7a4fc7b539ebcca9a6c78e2904ca53e633e649..2bbbd17af44cf460bbbc0b1e8d1139e9df2fbf38 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
@@ -10,12 +10,14 @@
"pattern": "to_uint64.2$x" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 4.6879,
- "steps": 46 } ],
- "No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid",
- "time": 4.8895,
- "steps": 47 } ] } } ],
+ "time": 6.9304,
+ "steps": 47 } ],
+ "Lower": [ { "prover": "qed",
+ "verdict": "valid" } ],
+ "Upper": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 5.6793,
+ "steps": 48 } ] } } ],
"Value 0": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-step",
@@ -25,12 +27,16 @@
"pattern": "to_uint64*$a$b" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 4.7487,
- "steps": 40 } ],
- "No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid",
- "time": 4.7716,
- "steps": 183 } ] } } ],
+ "time": 6.3679,
+ "steps": 184 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 5.8854,
+ "steps": 42 } ],
+ "Upper": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 6.2747,
+ "steps": 42 } ] } } ],
"Value 1": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-step",
@@ -40,12 +46,16 @@
"pattern": "to_uint64*$a$b" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 4.7262,
- "steps": 44 } ],
- "No-Overflow": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid",
- "time": 4.7611,
- "steps": 221 } ] } } ],
+ "time": 6.9832,
+ "steps": 222 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 6.0791,
+ "steps": 45 } ],
+ "Upper": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 5.1665,
+ "steps": 45 } ] } } ],
"Upper 1": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 6.2835,
+ "verdict": "valid", "time": 6.0617,
"steps": 48 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
new file mode 100644
index 0000000000000000000000000000000000000000..9ca995ee6234769c156b30223f2b7d8dcb67e964
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
@@ -0,0 +1,28 @@
+[ { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(to_uint32 c_0)", "pattern": "to_uint32$c" },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0094,
+ "steps": 25 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0238,
+ "steps": 53 },
+ { "header": "Overflow", "tactic": "Wp.overflow",
+ "params": {},
+ "select": { "select": "inside-goal",
+ "occur": 0,
+ "target": "(to_uint32\n (ui_0+((4294967296+c_0+(-4294967296*(c_0 div 4294967296))) mod 4294967296)))",
+ "pattern": "to_uint32+$ui%+42949672964294967296" },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 0.0166,
+ "steps": 27 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 0.023,
+ "steps": 25 } ],
+ "Upper": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 0.0739,
+ "steps": 73 } ] } } ],
+ "Upper": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
new file mode 100644
index 0000000000000000000000000000000000000000..b07a89798751525300ec38be4ef5de65ee73b4cb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
@@ -0,0 +1,28 @@
+[ { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(to_uint32 s_0)", "pattern": "to_uint32$s" },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0098,
+ "steps": 25 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0248,
+ "steps": 54 },
+ { "header": "Overflow", "tactic": "Wp.overflow",
+ "params": {},
+ "select": { "select": "inside-goal",
+ "occur": 0,
+ "target": "(to_uint32\n (ui_0+((4294967296+s_0+(-4294967296*(s_0 div 4294967296))) mod 4294967296)))",
+ "pattern": "to_uint32+$ui%+42949672964294967296" },
+ "children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 0.017,
+ "steps": 27 } ],
+ "Lower": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 0.0232,
+ "steps": 25 } ],
+ "Upper": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid",
+ "time": 0.2614,
+ "steps": 73 } ] } } ],
+ "Upper": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a8785509c81d41298eefab3cfbeb4f8afeb5df86
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
@@ -0,0 +1,13 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/overflow.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 2 goals scheduled
+[wp] [Script] Goal typed_lemma_j_incr_char : Valid
+[wp] [Script] Goal typed_lemma_j_incr_short : Valid
+[wp] Proved goals: 2 / 2
+ Qed: 0
+ Script: 2
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - - 2 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/overflow.i b/src/plugins/wp/tests/wp_tip/overflow.i
new file mode 100644
index 0000000000000000000000000000000000000000..3150b39720d4fca966f1455bdc02778faa3ad5f1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/overflow.i
@@ -0,0 +1,24 @@
+/* run.config
+ DONTRUN:
+*/
+
+/* run.config_qualif
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1
+*/
+
+typedef unsigned int uint;
+typedef unsigned short ushort;
+
+/*@
+ lemma j_incr_char:
+ \forall uint ui, char c;
+ 0 <= ui <= 1000 && 0 <= ui + c <= 1000 ==>
+ ui + c == (uint)(ui + (uint)(c)) ;
+*/
+
+/*@
+ lemma j_incr_short:
+ \forall uint ui, short s;
+ 0 <= ui <= 1000 && 0 <= ui + s <= 1000 ==>
+ ui + s == (uint)(ui + (uint)(s)) ;
+*/