From 8a3a7331ea70ebd6a7bf9310861927b46e9dacd4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 26 Apr 2019 13:30:18 +0200
Subject: [PATCH] [wp] no more support for -wp-no-bool-range
---
src/plugins/wp/Cint.ml | 42 ++++++++++++-------
src/plugins/wp/TacBitwised.ml | 2 +-
src/plugins/wp/ctypes.ml | 42 +++++++++----------
src/plugins/wp/ctypes.mli | 3 +-
.../tests/wp_acsl/oracle/bitwise.res.oracle | 10 ++---
src/plugins/wp/tests/wp_plugin/bool.i | 8 ++--
.../tests/wp_plugin/oracle/bool.0.res.oracle | 27 ++++++------
.../tests/wp_plugin/oracle/rte.0.res.oracle | 7 +---
src/plugins/wp/tests/wp_plugin/rte.i | 4 +-
src/plugins/wp/wpRTE.ml | 4 ++
src/plugins/wp/wp_parameters.ml | 9 ----
src/plugins/wp/wp_parameters.mli | 1 -
12 files changed, 78 insertions(+), 81 deletions(-)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 02c88290a4e..db97213a0c4 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -238,13 +238,14 @@ let match_power2_extraction = match_list_extraction match_power2
(* -------------------------------------------------------------------------- *)
(* rule A: to_a(to_b x) = to_b x when domain(b) is all included in domain(a) *)
-(* rule B: to_a(to_b x) = to_a x when size(b) is a multiple of size(a) *)
+(* rule B: to_a(to_b x) = to_a x when range(b) is a multiple of range(a)
+ AND a is not bool *)
-(* to_iota(e) where e = to_iota'(e') *)
-let simplify_f_to_conv f iota e conv e' =
+(* to_iota(e) where e = to_iota'(e'), only ranges for iota *)
+let simplify_range_comp f iota e conv e' =
let iota' = to_cint conv in
- let size' = Ctypes.i_bits iota' in
- let size = Ctypes.i_bits iota in
+ let size' = Ctypes.range iota' in
+ let size = Ctypes.range iota in
if size <= size'
then e_fun f [e']
(* rule B:
@@ -269,12 +270,12 @@ let simplify_f_to_bounds iota e =
let f_to_int = Ctypes.i_memo (fun iota -> make_fun_int "to" iota)
let configure_to_int iota =
- let f = f_to_int iota in
- let simplify e =
+
+ let simplify_range f iota e =
begin
try match F.repr e with
| Logic.Kint value ->
- let size = Integer.of_int (Ctypes.i_bits iota) in
+ let size = Integer.of_int (Ctypes.range iota) in
let signed = Ctypes.signed iota in
F.e_zint (Integer.cast ~size ~signed ~value)
| Logic.Fun( fland , es )
@@ -297,15 +298,22 @@ let configure_to_int iota =
| _ -> raise Not_found
end
| Logic.Fun( conv , [e'] ) -> (* unary op *)
- simplify_f_to_conv f iota e conv e'
+ simplify_range_comp f iota e conv e'
| _ -> raise Not_found
with Not_found ->
simplify_f_to_bounds iota e
end
in
- F.set_builtin_1 f simplify ;
-
- let simplify_leq x y =
+ let simplify_conv f iota e =
+ if iota = Ctypes.CBool then
+ match F.is_equal e F.e_zero with
+ | Yes -> F.e_zero
+ | No -> F.e_one
+ | Maybe -> raise Not_found
+ else
+ simplify_range f iota e
+ in
+ let simplify_leq f iota x y =
let lower,upper = Ctypes.bounds iota in
match F.repr y with
| Logic.Fun( conv , [_] )
@@ -324,7 +332,9 @@ let configure_to_int iota =
| _ -> raise Not_found
end
in
- F.set_builtin_leq f simplify_leq ;
+ let f = f_to_int iota in
+ F.set_builtin_1 f (simplify_conv f iota) ;
+ F.set_builtin_leq f (simplify_leq f iota) ;
to_cint_map := FunMap.add f iota !to_cint_map
@@ -485,14 +495,14 @@ let smp_bitk_positive = function
F.e_not (bitk_positive k a)
| Logic.Fun( conv , [a] ) (* when is_to_c_int conv *) ->
let iota = to_cint conv in
- let size = Ctypes.i_bits iota in
+ let range = Ctypes.range iota in
let signed = Ctypes.signed iota in
if signed then (* beware of sign-bit *)
- begin match is_leq k (e_int (size-2)) with
+ begin match is_leq k (e_int (range-2)) with
| Logic.Yes -> bitk_positive k a
| Logic.No | Logic.Maybe -> raise Not_found
end
- else begin match is_leq (e_int size) k with
+ else begin match is_leq (e_int range) k with
| Logic.Yes -> e_false
| Logic.No -> bitk_positive k a
| Logic.Maybe -> raise Not_found
diff --git a/src/plugins/wp/TacBitwised.ml b/src/plugins/wp/TacBitwised.ml
index bf9604878cc..c49c61d292f 100644
--- a/src/plugins/wp/TacBitwised.ml
+++ b/src/plugins/wp/TacBitwised.ml
@@ -108,7 +108,7 @@ let rec lookup push clause ~nbits ~priority p =
class autobitwise =
object(self)
- method private nbits = Ctypes.i_bits (Ctypes.c_ptr ())
+ method private nbits = Ctypes.range (Ctypes.c_ptr ())
method id = "wp:bitwised"
method title =
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index a108e37fd5a..f26b9025053 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -47,14 +47,14 @@ let signed = function
| UInt8 | UInt16 | UInt32 | UInt64 -> false
| SInt8 | SInt16 | SInt32 | SInt64 -> true
-let i_bits = function
- | CBool -> 8
+let range = function
+ | CBool -> 1
| UInt8 | SInt8 -> 8
| UInt16 | SInt16 -> 16
| UInt32 | SInt32 -> 32
| UInt64 | SInt64 -> 64
-let i_bytes = function
+let sizeof_i = function
| CBool -> 1
| UInt8 | SInt8 -> 1
| UInt16 | SInt16 -> 2
@@ -97,8 +97,8 @@ let c_ptr () =
make_c_int false Cil.theMachine.Cil.theMachine.sizeof_ptr
let sub_c_int t1 t2 =
- if (signed t1 = signed t2) then i_bits t1 <= i_bits t2
- else (not(signed t1) && (i_bits t1 < i_bits t2))
+ if (signed t1 = signed t2) then range t1 <= range t2
+ else (not(signed t1) && (range t1 < range t2))
type c_float =
| Float32
@@ -106,7 +106,7 @@ type c_float =
let compare_c_float : c_float -> c_float -> _ = Extlib.compare_basic
-let f_bytes = function
+let sizeof_f = function
| Float32 -> 4
| Float64 -> 8
@@ -126,7 +126,7 @@ let c_float fkind =
| FDouble -> make_c_float mach.sizeof_double
| FLongDouble -> make_c_float mach.sizeof_longdouble
-let equal_float f1 f2 = f_bits f1 = f_bits f2
+let equal_float f1 f2 = (f1 = f2)
(* Array objects, with both the head view and the flatten view. *)
@@ -195,15 +195,15 @@ let f_iter f =
(* --- Bounds --- *)
(* -------------------------------------------------------------------------- *)
-let i_bounds i =
- if signed i then
- let m = Integer.two_power_of_int (i_bits i - 1) in
- Integer.neg m , Integer.pred m
- else
- let m = Integer.two_power_of_int (i_bits i) in
- Integer.zero , Integer.pred m
-
-let bounds i = i_memo i_bounds i
+let bounds =
+ let i_bounds i =
+ if signed i then
+ let m = Integer.two_power_of_int (range i - 1) in
+ Integer.neg m , Integer.pred m
+ else
+ let m = Integer.two_power_of_int (range i) in
+ Integer.zero , Integer.pred m
+ in i_memo i_bounds
(* -------------------------------------------------------------------------- *)
(* --- Pretty Printers --- *)
@@ -211,7 +211,7 @@ let bounds i = i_memo i_bounds i
let pp_int fmt i =
if i = CBool then Format.pp_print_string fmt "bool"
- else Format.fprintf fmt "%cint%d" (if signed i then 's' else 'u') (i_bits i)
+ else Format.fprintf fmt "%cint%d" (if signed i then 's' else 'u') (range i)
let pp_float fmt f = Format.fprintf fmt "float%d" (f_bits f)
@@ -445,9 +445,9 @@ let sizeof_defined = function
| _ -> true
let sizeof_object = function
- | C_int i -> i_bytes i
- | C_float f -> f_bytes f
- | C_pointer _ty -> i_bytes (c_ptr())
+ | C_int i -> sizeof_i i
+ | C_float f -> sizeof_f f
+ | C_pointer _ty -> sizeof_i (c_ptr())
| C_comp cinfo ->
let ctype = TComp(cinfo,Cil.empty_size_cache(),[]) in
(Cil.bitsSizeOf ctype / 8)
@@ -490,7 +490,7 @@ let field_offset fd =
(* with greater rank, whatever *)
(* their sign. *)
-let i_convert t1 t2 = if i_bits t1 < i_bits t2 then t2 else t1
+let i_convert t1 t2 = if range t1 < range t2 then t2 else t1
let f_convert t1 t2 = if f_bits t1 < f_bits t2 then t2 else t1
let promote a1 a2 =
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index bb3c965c1bd..b09df11064c 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/src/plugins/wp/ctypes.mli
@@ -97,9 +97,8 @@ val char : char -> int64
val constant : exp -> int64
val get_int : exp -> int64 option
-val i_bits : c_int -> int (** size in bits *)
-val i_bytes : c_int -> int (** size in bytes *)
val signed : c_int -> bool (** [true] if signed *)
+val range : c_int -> int (** range in 2^n *)
val bounds: c_int -> Integer.t * Integer.t (** domain, bounds included *)
(** All sizes are in bits *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
index 789c01a6f59..70d1558a270 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -76,7 +76,7 @@ Prove: land(65535, a) != 21845.
Goal Post-condition for 'false' (file tests/wp_acsl/bitwise.i, line 91) in 'band_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'false' *)
Have: (a != 1) \/ (b != 1).
}
@@ -142,7 +142,7 @@ Prove: true.
Goal Post-condition for 'false' (file tests/wp_acsl/bitwise.i, line 81) in 'bor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'false' *)
Have: (a != 1) /\ (b != 1).
}
@@ -155,7 +155,7 @@ Prove: (a = 0) /\ (b = 0).
Goal Post-condition for 'true' (file tests/wp_acsl/bitwise.i, line 78) in 'bor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'true' *)
Have: (a = 1) \/ (b = 1).
}
@@ -202,7 +202,7 @@ Prove: lnot(x) = b.
Goal Post-condition for 'false' (file tests/wp_acsl/bitwise.i, line 100) in 'bxor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'false' *)
Have: ((a != 0) \/ (b != 1)) /\ ((a != 1) \/ (b != 0)).
}
@@ -215,7 +215,7 @@ Prove: b = a.
Goal Post-condition for 'true' (file tests/wp_acsl/bitwise.i, line 97) in 'bxor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'true' *)
Have: ((a = 0) /\ (b = 1)) \/ ((a = 1) /\ (b = 0)).
}
diff --git a/src/plugins/wp/tests/wp_plugin/bool.i b/src/plugins/wp/tests/wp_plugin/bool.i
index 929c6448995..0b90b861d07 100644
--- a/src/plugins/wp/tests/wp_plugin/bool.i
+++ b/src/plugins/wp/tests/wp_plugin/bool.i
@@ -1,11 +1,11 @@
/* run.config
- OPT: -wp-no-let -wp-no-bool-range
- OPT: -wp-no-let -wp-bool-range
+ OPT: -wp-no-let
+ OPT: -wp-no-let
*/
/* run.config_qualif
- OPT: -wp-no-let -wp-no-bool-range
- OPT: -wp-no-let -wp-bool-range
+ OPT: -wp-no-let
+ OPT: -wp-no-let
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle
index 68874ceaf82..feb6965058e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle
@@ -9,8 +9,8 @@
Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 30) in 'band_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(band_bool_0) /\ is_uint8(retres_0).
+ Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
+ is_bool(band_bool_0) /\ is_bool(retres_0).
Have: (a_1 = a) /\ (b_1 = b).
(* Pre-condition for 'false' *)
Have: (a_1 != 1) \/ (b_1 != 1).
@@ -27,8 +27,8 @@ Prove: band_bool_0 = 0.
Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 27) in 'band_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(band_bool_0) /\ is_uint8(retres_0).
+ Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
+ is_bool(band_bool_0) /\ is_bool(retres_0).
Have: (a_1 = a) /\ (b_1 = b).
(* Pre-condition for 'true' *)
Have: (a_1 = 1) /\ (b_1 = 1).
@@ -45,8 +45,8 @@ Prove: band_bool_0 = 1.
Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 20) in 'bor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(bor_bool_0) /\ is_uint8(retres_0).
+ Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
+ is_bool(bor_bool_0) /\ is_bool(retres_0).
Have: (a_1 = a) /\ (b_1 = b).
(* Pre-condition for 'false' *)
Have: (a_1 != 1) /\ (b_1 != 1).
@@ -63,8 +63,8 @@ Prove: bor_bool_0 = 0.
Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 17) in 'bor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(bor_bool_0) /\ is_uint8(retres_0).
+ Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
+ is_bool(bor_bool_0) /\ is_bool(retres_0).
Have: (a_1 = a) /\ (b_1 = b).
(* Pre-condition for 'true' *)
Have: (a_1 = 1) \/ (b_1 = 1).
@@ -81,8 +81,8 @@ Prove: bor_bool_0 = 1.
Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 39) in 'bxor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(bxor_bool_0) /\ is_uint8(retres_0).
+ Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
+ is_bool(bxor_bool_0) /\ is_bool(retres_0).
Have: (a_1 = a) /\ (b_1 = b).
(* Pre-condition for 'false' *)
Have: ((a_1 != 0) \/ (b_1 != 1)) /\ ((a_1 != 1) \/ (b_1 != 0)).
@@ -99,8 +99,8 @@ Prove: bxor_bool_0 = 0.
Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 36) in 'bxor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(bxor_bool_0) /\ is_uint8(retres_0).
+ Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
+ is_bool(bxor_bool_0) /\ is_bool(retres_0).
Have: (a_1 = a) /\ (b_1 = b).
(* Pre-condition for 'true' *)
Have: ((a_1 = 0) /\ (b_1 = 1)) \/ ((a_1 = 1) /\ (b_1 = 0)).
@@ -117,8 +117,7 @@ Prove: bxor_bool_0 = 1.
Goal Post-condition (file tests/wp_plugin/bool.i, line 12) in 'job':
Assume {
- Type: is_uint8(a) /\ is_uint8(b) /\ is_sint32(job_0) /\
- is_sint32(retres_0).
+ Type: is_bool(a) /\ is_bool(b) /\ is_sint32(job_0) /\ is_sint32(retres_0).
Have: (a + b) = retres_0.
(* Return *)
Have: retres_0 = job_0.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
index 00dfe9f2904..64040ba3823 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
@@ -14,10 +14,7 @@
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
[rte] annotating function job3
-[wp] tests/wp_plugin/rte.i:34: Warning:
- Option -wp-bool-range incompatiable with RTE (ignored)
-[wp] tests/wp_plugin/rte.i:34: Warning:
- Option -wp-bool-range incompatiable with RTE (ignored)
+[wp] Warning: memory model incompatible with -no-warn-invalid-bool
[wp] Goal typed_job_ensures : not tried
[wp] Goal typed_job_assert_rte_mem_access : not tried
[wp] Goal typed_job_assert_rte_mem_access_2 : not tried
@@ -26,7 +23,6 @@
[wp] Goal typed_job_assert_rte_mem_access_3 : not tried
[wp] Goal typed_job2_ensures : not tried
[wp] Goal typed_job3_ensures : not tried
-[wp] Goal typed_job3_assert_rte_bool_value : not tried
/* Generated by Frama-C */
/*@ axiomatic Obs {
predicate R(integer r) ;
@@ -60,7 +56,6 @@ _Bool X;
int job3(void)
{
int __retres;
- /*@ assert rte: bool_value: X == 0 || X == 1; */
__retres = (int)X;
return __retres;
}
diff --git a/src/plugins/wp/tests/wp_plugin/rte.i b/src/plugins/wp/tests/wp_plugin/rte.i
index f20717efcba..1b63b3768c8 100644
--- a/src/plugins/wp/tests/wp_plugin/rte.i
+++ b/src/plugins/wp/tests/wp_plugin/rte.i
@@ -1,6 +1,6 @@
/* run.config
CMD: @frama-c@ -wp -wp-prover none -wp-check -wp-share ./share -wp-msg-key shell -wp-msg-key rte
- OPT: -wp-rte -warn-invalid-bool -wp-bool-range -then -print -no-unicode
+ OPT: -wp-rte -no-warn-invalid-bool -then -print -no-unicode
OPT: -wp-rte -no-warn-signed-overflow -then -print -no-unicode
OPT: -wp-rte -warn-unsigned-overflow -then -print -no-unicode
OPT: -wp-rte -wp-model +nat -then -print -no-unicode
@@ -9,7 +9,7 @@
OPT: -wp-rte -rte-no-mem -wp-model +nat
*/
/* run.config_qualif
- OPT: -wp-rte -warn-invalid-bool -wp-bool-range -wp-prop=rte
+ OPT: -wp-rte -warn-invalid-bool -wp-prop=rte
*/
diff --git a/src/plugins/wp/wpRTE.ml b/src/plugins/wp/wpRTE.ml
index 30974a1edba..e373289c57a 100644
--- a/src/plugins/wp/wpRTE.ml
+++ b/src/plugins/wp/wpRTE.ml
@@ -102,4 +102,8 @@ let missing_guards kf model =
let update = ref false in
let cint = Model.with_model model Cint.current () in
List.iter (configure ~update ~generate:false kf cint) generator ;
+ let has_bool_traps = not (Kernel.InvalidBool.get ()) in
+ if has_bool_traps then
+ Wp_parameters.warning ~once:true ~current:false
+ "memory model incompatible with -no-warn-invalid-bool" ;
!update
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 3ea59dcff6c..6e8fc4bb53d 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -223,14 +223,6 @@ module ExtEqual =
let help = "Use extensional equality on compounds (hypotheses only)."
end)
-let () = Parameter_customize.set_group wp_model
-let () = Parameter_customize.is_invisible () (* experimental option *)
-module BoolRange =
- False(struct
- let option_name = "-wp-bool-range"
- let help = "Assumes _Bool values have no trap representations."
- end)
-
let () = Parameter_customize.set_group wp_model
module Overflows =
False(struct
@@ -909,7 +901,6 @@ let active_unless_rte option =
else true
let get_overflows () = Overflows.get () && active_unless_rte "-wp-overflows"
-let get_bool_range () = BoolRange.get () && active_unless_rte "-wp-bool-range"
let dkey = register_category "env"
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 88dfd0553b3..d9fd672e9b5 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -146,7 +146,6 @@ val get_output : unit -> string
val get_output_dir : string -> string
val get_includes : unit -> string list
val make_output_dir : string -> unit
-val get_bool_range : unit -> bool
val get_overflows : unit -> bool
(** {2 Debugging Categories} *)
--
GitLab