diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml index 02c88290a4e5bf52db262ee8661d51cce8d337a2..db97213a0c468ae98b411ac54309ac9ee440f8c3 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 bf9604878cc9858d958d7d8fde96ac300cfd9983..c49c61d292fe3732c9642389b32c1ce581cea0c6 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 a108e37fd5a81394135a15b09405b0312cbb09d7..f26b90250538d28231b9fbbee1bd422d4f3fe95d 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 bb3c965c1bd887c4aaf998d53e573a845ac0715d..b09df11064c7352f237ebc29997f42b18528b8a3 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 789c01a6f59aa4dd26ca8c135f21bd2f89370f1b..70d1558a270afd984352f05fee911ed8f71bc1c3 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 929c64489953a8bc22f2b39f9db7667cf080bda6..0b90b861d0755fbcf83b2a704389f49683cd6dc3 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 68874ceaf821d834a858885852f28ca43f628961..feb6965058e45327d31bd7bcea1975946210b74e 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 00dfe9f2904865a995c497204fcbe1dee0d229d1..64040ba38238b5a5b56201dd53d87523b491b9a3 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 f20717efcbadf7f1ea1be762af3fb9e605b0e142..1b63b3768c83f5e7f9f053f2bf203a2a879e0851 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 30974a1edba460c7bed8feb8f91a76105ffb5afc..e373289c57ad382746274a59d2df04fcb168241c 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 3ea59dcff6c5d945d25a6a9f9ab253da7373cd73..6e8fc4bb53dbaee7e025a402786555b89db78604 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 88dfd0553b3f8aea5e6db86da44a6c4a8de29157..d9fd672e9b5225aaed8973ac6ec9678175ded356 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} *)