Commit b8d27920 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch '963-wp-corner-cases-with-bitwise-mask' into 'master'

Resolve "[wp] Corner cases with bitwise mask"

Closes #963

See merge request frama-c/frama-c!2877
parents c02e95ab 7c755c55
......@@ -1611,6 +1611,8 @@ src/plugins/wp/TacBitwised.ml: CEA_WP
src/plugins/wp/TacBitwised.mli: CEA_WP
src/plugins/wp/TacBitrange.ml: CEA_WP
src/plugins/wp/TacBitrange.mli: CEA_WP
src/plugins/wp/TacBittest.ml: CEA_WP
src/plugins/wp/TacBittest.mli: CEA_WP
src/plugins/wp/TacChoice.ml: CEA_WP
src/plugins/wp/TacChoice.mli: CEA_WP
src/plugins/wp/TacCongruence.ml: CEA_WP
......
......@@ -24,6 +24,7 @@
Plugin WP <next-release>
#########################
- WP [2020-10-07] New tactic Bit-Test range
- WP [2020-09-21] Added support for Why3 interactive prover (Coq)
- WP [2020-09-21] New option -wp-interactive <mode>
- WP [2020-09-21] New option -wp-interactive-timeout <seconds>
......
......@@ -89,7 +89,7 @@ PLUGIN_CMO:= \
TacArray TacCompound TacUnfold \
TacHavoc TacInstance TacLemma \
TacFilter TacCut WpTac TacNormalForm \
TacRewrite TacBitwised TacBitrange TacShift \
TacRewrite TacBitwised TacBitrange TacBittest TacShift \
TacCongruence TacOverflow Auto \
ProofSession ProofScript ProofEngine \
ProverTask ProverErgo ProverCoq \
......
......@@ -89,8 +89,10 @@ let search tree ?anchor ?sequent heuristics =
let anchor = ProofEngine.anchor tree ?node:anchor () in
let sequent =
match sequent with
| Some s -> s | None -> snd (Wpo.compute (ProofEngine.goal anchor)) in
| Some s -> s
| None -> snd (Wpo.compute (ProofEngine.goal anchor)) in
let lookup h = try h#search pool#add sequent with Not_found -> () in
Conditions.index sequent ;
WpContext.on_context
(ProofEngine.node_context anchor)
(List.iter lookup) heuristics ;
......
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2020 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Lang
(* -------------------------------------------------------------------------- *)
(* --- Helpers --- *)
(* -------------------------------------------------------------------------- *)
let positive e = F.p_leq F.e_zero e (* 0 <= n *)
let power k = F.e_bigint (Integer.two_power_of_int k)
let lookup_int e =
let open Qed.Logic in
match F.repr e with
| Kint z -> (try Some (Integer.to_int z) with Z.Overflow -> None)
| _ -> None
let rec lookup_bittest e =
match F.repr e with
| Not e -> lookup_bittest e
| Fun(f,[n;ek]) when List.memq f Cint.f_bits ->
begin
match lookup_int ek with
| Some k when 0 <= k && k < 128 -> Some (n,k)
| _ -> None
end
| _ -> None
(* -------------------------------------------------------------------------- *)
(* --- Bit-Test Range --- *)
(* -------------------------------------------------------------------------- *)
class bittestrange =
object
inherit Tactical.make
~id:"Wp.bittestrange"
~title:"Bit-Test Range"
~descr:"Tighten Bounds with respect to bits"
~params:[]
method select _feedback selection =
let e = Tactical.selected selection in
match lookup_bittest e with
| Some (n,k) ->
let bit = Cint.bit_test n k in
let bit_set = F.p_bool bit in
let bit_clear = F.p_not bit_set in
let pos = positive n in
let pk = power k in
let pk1 = power (succ k) in
let g_inf = F.p_hyps [pos] (F.p_leq pk n) in
let g_sup = F.p_hyps [pos;F.p_lt n pk1] (F.p_lt n pk) in
let name_inf = Printf.sprintf "Bit #%d (inf)" k in
let name_sup = Printf.sprintf "Bit #%d (sup)" k in
let at = Tactical.at selection in
Tactical.Applicable (Tactical.insert ?at [
name_inf , F.p_and bit_set g_inf ;
name_sup , F.p_and bit_clear g_sup ;
])
| None -> Tactical.Not_applicable
end
let tactical = Tactical.export (new bittestrange)
let strategy = Strategy.make tactical ~arguments:[]
(* -------------------------------------------------------------------------- *)
(* --- Auto Bitrange --- *)
(* -------------------------------------------------------------------------- *)
let rec lookup push step e =
match F.repr e with
| And es -> List.iter (lookup push step) es
| Or es -> List.iter (lookup push step) es
| Imply (hs,p) -> List.iter (lookup push step) (p::hs)
| _ ->
begin
match lookup_bittest e with
| None -> ()
| Some _ ->
push @@ strategy ~priority:0.3 (Tactical.Inside(step,e))
end
class autobittestrange : Strategy.heuristic =
object
method id = "wp:bittestrange"
method title = "Auto Bit-Test Range"
method descr = "Apply Bit-Test Range on bit-tests"
method search push (seq : Conditions.sequent) =
Conditions.iter
(fun step ->
let p = Conditions.head step |> F.e_prop in
lookup push (Tactical.Step step) p
) (fst seq) ;
let p = snd seq in
lookup push (Tactical.Goal p) (F.e_prop p)
end
let () = Strategy.register (new autobittestrange)
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2007-2020 *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
(** Built-in Bit-Test Range Tactical (auto-registered) *)
open Tactical
open Strategy
val tactical : tactical
val strategy : ?priority:float -> selection -> strategy
(**************************************************************************)
/* run.config
DONTRUN:
*/
/* run.config_qualif
OPT: -wp-prover script,alt-ergo
*/
typedef unsigned short ushort;
/*@
lemma res_n: \forall ushort off; ! (off & 0x8000) ==> off < 0x8000;
lemma res_y: \forall ushort off; (off & 0x8000) ==> off >= 0x8000;
*/
[ { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
"select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "not (bit_test off_0 15)",
"pattern": "!bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "qed", "verdict": "valid" } ],
"Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.0203,
"steps": 21 } ] } } ]
[ { "header": "Bit-Test Range", "tactic": "Wp.bittestrange", "params": {},
"select": { "select": "inside-step", "at": 1, "kind": "have", "occur": 0,
"target": "(bit_test off_0 15)",
"pattern": "bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.0.0",
"verdict": "valid", "time": 0.0214,
"steps": 20 } ],
"Bit #15 (sup)": [ { "prover": "qed", "verdict": "valid" } ] } } ]
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/bitmask0x8000.h (with preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Script] Goal typed_lemma_res_n : Valid
[wp] [Script] Goal typed_lemma_res_y : Valid
[wp] Proved goals: 2 / 2
Qed: 0
Script: 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 2 100%
------------------------------------------------------------
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment