diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
index 0a7b37dcc03a4c242e47d0e37968bd74c598eb95..4d35f6a6a678191b21d4f63da3969eb28169a327 100644
--- a/nix/mk_tests.nix
+++ b/nix/mk_tests.nix
@@ -26,6 +26,7 @@
{ lib
, alt-ergo
+, cvc4
, clang
, frama-c
, perl
@@ -60,7 +61,7 @@ stdenvNoCC.mkDerivation {
yq
which
] ++
- (if has-wp-proofs then [ alt-ergo ] else []);
+ (if has-wp-proofs then [ alt-ergo cvc4 ] else []);
postPatch = ''
patchShebangs .
diff --git a/src/libraries/utils/bag.ml b/src/libraries/utils/bag.ml
index 59dea90c400108ba97e69fe0d9fa31d23ba3b067..83d9273ce7ad3c7bc48c66355ae58b5bc444e0c2 100644
--- a/src/libraries/utils/bag.ml
+++ b/src/libraries/utils/bag.ml
@@ -97,6 +97,37 @@ let rec iter f = function
| List xs -> List.iter f xs
| Concat(a,b) -> iter f a ; iter f b
+let find (type a) f xs =
+ let exception Found of a in
+ try
+ iter (fun x -> if f x then raise (Found x)) xs ;
+ raise Not_found
+ with Found x -> x
+
+let find_opt (type a) f xs =
+ let exception Found of a in
+ try
+ iter (fun x -> if f x then raise (Found x)) xs ;
+ None
+ with Found x -> Some x
+
+let find_map (type b) f xs =
+ let exception Found of b in
+ try
+ iter (fun x -> match f x with Some y -> raise (Found y) | None -> ()) xs ;
+ None
+ with Found x -> Some x
+
+let exists f xs =
+ let exception Found in
+ try iter (fun x -> if f x then raise Found) xs ; false
+ with Found -> true
+
+let for_all f xs =
+ let exception Found in
+ try iter (fun x -> if not @@ f x then raise Found) xs ; true
+ with Found -> false
+
let rec fold_left f w = function
| Empty -> w
| Elt x -> f w x
diff --git a/src/libraries/utils/bag.mli b/src/libraries/utils/bag.mli
index 0dfb4c34ce16c43b4591dcffc2f05c711e42403a..4c9e704b23f688969a974b6fca08e601ef9cc841 100644
--- a/src/libraries/utils/bag.mli
+++ b/src/libraries/utils/bag.mli
@@ -42,6 +42,17 @@ val iter : ('a -> unit) -> 'a t -> unit
val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+val find : ('a -> bool) -> 'a t -> 'a
+val find_opt : ('a -> bool) -> 'a t -> 'a option
+val find_map : ('a -> 'b option) -> 'a t -> 'b option
+(** [find_map f b]: finds the first element [x] of the bag such
+ that [f x] returns [Some y], and returns [Some y]. If no such
+ element exists, returns None.
+*)
+
+val exists : ('a -> bool) -> 'a t -> bool
+val for_all : ('a -> bool) -> 'a t -> bool
+
val filter : ('a -> bool) -> 'a t -> 'a t
val partition : ('a -> bool) -> 'a t -> 'a t * 'a t
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 5e7988978a2a4bd7ef7e975dcd002bf1ba3522ee..3ee82fe8b4aea89b7d1ec7a6d6de393a42d5f709 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -156,7 +156,7 @@ let steps_seized steps steplimit =
let promote ?timeout ?steplimit (res : VCS.result) =
match res.verdict with
- | VCS.NoResult | VCS.Computing _ | VCS.Failed -> VCS.no_result
+ | VCS.NoResult | VCS.Computing _ | VCS.Invalid | VCS.Failed -> VCS.no_result
| VCS.Valid | VCS.Unknown ->
if not (steps_fits res.prover_steps steplimit) then
{ res with verdict = Stepout }
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index c16ff02fa861910b652cb905e9b218f2da7d25c9..e3b12412e74b8dd0e5e849f4ae71308b5408d84d 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,10 @@
Plugin WP <next-release>
###############################################################################
+- WP [2024-01-24] Introduce counter examples via the new option
+ -wp-counter-examples. Also introduce an ACSL extension
+ to create probes on terms for counter examples.
+
###############################################################################
Plugin WP 28.0 (Nickel)
###############################################################################
diff --git a/src/plugins/wp/Cleaning.ml b/src/plugins/wp/Cleaning.ml
index 2672d901653a8a7498bd42ea20f75ec1b077648c..6343457d294e1e33596314f5bfbe4373d0d05730 100644
--- a/src/plugins/wp/Cleaning.ml
+++ b/src/plugins/wp/Cleaning.ml
@@ -50,7 +50,8 @@ let cup_false = function
| FALSE -> FALSE
| _ -> TOP
-let set_top m p = Vars.fold (fun x m -> Vmap.add x TOP m) (F.varsp p) m
+let add_term m t = Vars.fold (fun x m -> Vmap.add x TOP m) (F.vars t) m
+let add_prop m p = add_term m (F.e_prop p)
let add eq x d m = Vmap.add x (try cup eq (Vmap.find x m) d with Not_found -> EQ d) m
let add_true m x = Vmap.add x (try cup_true (Vmap.find x m) with Not_found -> TRUE) m
let add_false m x = Vmap.add x (try cup_false (Vmap.find x m) with Not_found -> FALSE) m
@@ -64,21 +65,21 @@ let add_fun = add Fun.equal
let rec add_pred m p =
match F.p_expr p with
| And ps -> List.fold_left add_pred m ps
- | If(e,a,b) -> add_pred (add_pred (set_top m e) a) b
+ | If(e,a,b) -> add_pred (add_pred (add_prop m e) a) b
| Eq(a,b) ->
begin
match F.p_expr a , F.p_expr b with
| Fvar x , Fvar y -> add_var x y (add_var y x m)
- | _ -> set_top m p
+ | _ -> add_prop m p
end
| Fvar x -> add_true m x
| Not p ->
begin
match F.p_expr p with
| Fvar x -> add_false m x
- | _ -> set_top m p
+ | _ -> add_prop m p
end
- | _ -> set_top m p
+ | _ -> add_prop m p
let rec add_type m p =
match F.p_expr p with
@@ -87,9 +88,9 @@ let rec add_type m p =
begin
match F.e_expr e with
| Fvar x -> add_fun x f m
- | _ -> set_top m p
+ | _ -> add_prop m p
end
- | _ -> set_top m p
+ | _ -> add_prop m p
(* -------------------------------------------------------------------------- *)
(* --- Usage --- *)
@@ -101,7 +102,8 @@ type usage = {
}
let create () = { eq_var = Vmap.empty ; eq_fun = Vmap.empty }
-let as_atom m p = m.eq_var <- set_top m.eq_var p
+let as_term m t = m.eq_var <- add_term m.eq_var t
+let as_atom m p = m.eq_var <- add_prop m.eq_var p
let as_have m p = m.eq_var <- add_pred m.eq_var p
let as_init m p = m.eq_fun <- add_type m.eq_fun p
let as_type m p = m.eq_fun <- add_type m.eq_fun p
diff --git a/src/plugins/wp/Cleaning.mli b/src/plugins/wp/Cleaning.mli
index 091b78fd0269e6626660c9ca0decd2d520c599d0..e849aeb991ebac991c142dbc9ea81a5133af8232 100644
--- a/src/plugins/wp/Cleaning.mli
+++ b/src/plugins/wp/Cleaning.mli
@@ -29,6 +29,7 @@ open Lang.F
type usage
val create : unit -> usage
+val as_term : usage -> term -> unit
val as_atom : usage -> pred -> unit
val as_type : usage -> pred -> unit
val as_have : usage -> pred -> unit
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 5947885c463bfd83cdf9eb24fc5f770ce7f45cff..bb251b1e1789b5725c01c33d46a3261ee25cc7d3 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -36,7 +36,7 @@ let dkey_pruning = Wp_parameters.register_category "pruning"
(* -------------------------------------------------------------------------- *)
type category =
- | EMPTY (** Empty Sequence, equivalent to True, but with State. *)
+ | KEEP (** Has probes, but equivalent to True *)
| TRUE (** Logically equivalent to True *)
| FALSE (** Logically equivalent to False *)
| MAYBE (** Any Hypothesis *)
@@ -45,13 +45,12 @@ let c_and c1 c2 =
match c1 , c2 with
| FALSE , _ | _ , FALSE -> FALSE
| MAYBE , _ | _ , MAYBE -> MAYBE
- | TRUE , _ | _ , TRUE -> TRUE
- | EMPTY , EMPTY -> EMPTY
+ | TRUE , TRUE -> TRUE
+ | (KEEP | TRUE) , (KEEP | TRUE) -> KEEP
let c_or c1 c2 =
match c1 , c2 with
| FALSE , FALSE -> FALSE
- | EMPTY , EMPTY -> EMPTY
| TRUE , TRUE -> TRUE
| _ -> MAYBE
@@ -61,7 +60,7 @@ let rec cfold_and a f = function
let rec cfold_or a f = function
| [] -> a | e::es -> cfold_or (c_or a (f e)) f es
-let c_conj f es = cfold_and EMPTY f es
+let c_conj f es = cfold_and TRUE f es
let c_disj f = function [] -> FALSE | e::es -> cfold_or (f e) f es
(* -------------------------------------------------------------------------- *)
@@ -85,6 +84,7 @@ and sequence = {
seq_catg : category ;
seq_list : step list ; (* forall i . 0 <= i < n ==> Step_i *)
}
+
and condition =
| Type of pred (* related to Type *)
| Have of pred
@@ -94,6 +94,7 @@ and condition =
| Branch of pred * sequence * sequence (* if Pred then Seq_1 else Seq_2 *)
| Either of sequence list (* exist i . 0 <= i < n && Sequence_i *)
| State of Mstate.state
+ | Probe of Probe.t * term
(* -------------------------------------------------------------------------- *)
(* --- Variable Utilities --- *)
@@ -107,8 +108,9 @@ let vars_cond = function
| Branch(p,sa,sb) -> Vars.union (F.varsp p) (Vars.union sa.seq_vars sb.seq_vars)
| Either cases -> vars_seqs cases
| State _ -> Vars.empty
+ | Probe(_,t) -> F.vars t
let size_cond = function
- | Type _ | When _ | Have _ | Core _ | Init _ | State _ -> 1
+ | Type _ | When _ | Have _ | Core _ | Init _ | State _ | Probe _ -> 1
| Branch(_,sa,sb) -> 1 + sa.seq_size + sb.seq_size
| Either cases -> List.fold_left (fun n s -> n + s.seq_size) 1 cases
let vars_hyp hs = hs.seq_vars
@@ -128,7 +130,7 @@ let rec add_core s p = match F.p_expr p with
| _ -> if is_core p then Pset.add p s else s
let core_cond = function
- | Type _ | State _ -> Pset.empty
+ | Type _ | State _ | Probe _ -> Pset.empty
| Have p | When p | Core p | Init p -> add_core Pset.empty p
| Branch(_,sa,sb) -> Pset.inter sa.seq_core sb.seq_core
| Either [] -> Pset.empty
@@ -146,12 +148,13 @@ let core_list s = List.fold_left add_core_step Pset.empty s
let catg_seq s = s.seq_catg
let catg_cond = function
| State _ -> TRUE
+ | Probe _ -> KEEP
| Have p | Type p | When p | Core p | Init p ->
begin
match F.is_ptrue p with
| No -> FALSE
| Maybe -> MAYBE
- | Yes -> EMPTY
+ | Yes -> TRUE
end
| Either cs -> c_disj catg_seq cs
| Branch(_,a,b) -> c_or a.seq_catg b.seq_catg
@@ -174,8 +177,10 @@ let sequence l = {
(* --- Sequence Comparator --- *)
(* -------------------------------------------------------------------------- *)
+(* Only used for stability after a turn of simpliciations *)
let rec equal_cond ca cb =
match ca,cb with
+ | Probe(p,a) , Probe(q,b) -> Probe.equal p q && a == b
| State _ , State _ -> true
| Type p , Type q
| Have p , Have q
@@ -187,6 +192,7 @@ let rec equal_cond ca cb =
p == q && equal_seq a a' && equal_seq b b'
| Either u, Either v ->
Qed.Hcons.equal_list equal_seq u v
+ | Probe _ , _ | _ , Probe _
| State _ , _ | _ , State _
| Type _ , _ | _ , Type _
| Have _ , _ | _ , Have _
@@ -221,7 +227,7 @@ struct
| Have p -> Have (fpred core p)
| When p -> When (fpred core p)
| Init p -> Init (fpred core p)
- | (Type _ | Branch _ | Either _ | State _) as cond -> cond
+ | (Type _ | Branch _ | Either _ | State _ | Probe _) as cond -> cond
let fstep core step =
let condition = fcond core step.condition in
@@ -319,18 +325,18 @@ let pretty = ref (fun _fmt _seq -> ())
let equal (a : sequent) (b : sequent) : bool =
F.eqp (snd a) (snd b) && equal_seq (fst a) (fst b)
-let is_true = function { seq_catg = TRUE | EMPTY } -> true | _ -> false
-let is_empty = function { seq_catg = EMPTY } -> true | _ -> false
+let is_true = function { seq_catg = TRUE | KEEP } -> true | _ -> false
+let is_empty = function { seq_catg = TRUE } -> true | _ -> false
let is_false = function { seq_catg = FALSE } -> true | _ -> false
let is_absurd_h h = match h.condition with
+ | State _ | Probe _ -> false
| (Type p | Core p | When p | Have p | Init p) -> p == F.p_false
| Branch(_,p,q) -> is_false p && is_false q
| Either w -> List.for_all is_false w (* note: an empty w is an absurd hyp *)
- | State _ -> false
let is_trivial_h h = match h.condition with
- | State _ -> false
+ | State _ | Probe _ -> false
| (Type p | Core p | When p | Have p | Init p) -> p == F.p_true
| Branch(_,a,b) -> is_true a && is_true b
| Either [] -> false
@@ -345,7 +351,7 @@ let is_trivial (s:sequent) = is_trivial_hs_p (fst s).seq_list (snd s)
(* -------------------------------------------------------------------------- *)
let rec pred_cond = function
- | State _ -> F.p_true
+ | State _ | Probe _ -> F.p_true
| When p | Type p | Have p | Core p | Init p -> p
| Branch(p,a,b) -> F.p_if p (pred_seq a) (pred_seq b)
| Either cases -> F.p_any pred_seq cases
@@ -394,11 +400,11 @@ let update_cond ?descr ?(deps=[]) ?(warn=Warning.Set.empty) h c =
type 'a disjunction = D_TRUE | D_FALSE | D_EITHER of 'a list
let disjunction phi es =
- let positives = ref false in (* TRUE or EMPTY items *)
+ let positives = ref false in (* TRUE or KEEP items *)
let remains = List.filter
(fun e ->
match phi e with
- | TRUE | EMPTY -> positives := true ; false
+ | TRUE | KEEP -> positives := true ; false
| MAYBE -> true
| FALSE -> false
) es in
@@ -531,9 +537,11 @@ let intros ps hs =
Bundle.add (step ~descr:"Goal" (When p)) hs
let state ?descr ?stmt state hs =
- let cond = State state in
- let s = step ?descr ?stmt cond in
- Bundle.add s hs
+ Bundle.add (step ?descr ?stmt (State state)) hs
+
+let probe ~loc ?descr ?stmt ~name term hs =
+ let p = Probe.create ~loc ?stmt ~name () in
+ Bundle.add (step ?descr ?stmt (Probe(p,term))) hs
let assume ?descr ?stmt ?deps ?warn ?(init=false) ?(domain=false) p hs =
match F.is_ptrue p with
@@ -545,7 +553,7 @@ let assume ?descr ?stmt ?deps ?warn ?(init=false) ?(domain=false) p hs =
| Maybe ->
begin
match Bundle.category hs with
- | MAYBE | TRUE | EMPTY ->
+ | MAYBE | TRUE | KEEP ->
let p = exist_intro p in
let cond =
if init then Init p else if domain then Type p else Have p in
@@ -600,10 +608,10 @@ let merge cases = either ~descr:"Merge" cases
(* -------------------------------------------------------------------------- *)
let rec flat_catg = function
- | [] -> EMPTY
+ | [] -> TRUE
| s::cs ->
match catg_step s with
- | EMPTY -> flat_catg cs
+ | TRUE -> flat_catg cs
| r -> r
let flat_cons step tail =
@@ -613,13 +621,13 @@ let flat_cons step tail =
let flat_concat head tail =
match flat_catg head with
- | EMPTY -> tail
+ | TRUE -> tail
| FALSE -> head
- | MAYBE|TRUE ->
+ | MAYBE|KEEP ->
match flat_catg tail with
- | EMPTY -> head
+ | TRUE -> head
| FALSE -> tail
- | MAYBE|TRUE -> head @ tail
+ | MAYBE|KEEP -> head @ tail
let core_residual step core = {
id = noid ;
@@ -635,7 +643,7 @@ let core_residual step core = {
let core_branch step p a b =
let condition =
match a.seq_catg , b.seq_catg with
- | (TRUE | EMPTY) , (TRUE|EMPTY) -> Have p_true
+ | (TRUE | KEEP) , (TRUE|KEEP) -> Have p_true
| FALSE , FALSE -> Have p_false
| _ -> Branch(p,a,b)
in update_cond step condition
@@ -644,7 +652,7 @@ let rec flatten_sequence m = function
| [] -> []
| step :: seq ->
match step.condition with
- | State _ -> flat_cons step (flatten_sequence m seq)
+ | State _ | Probe _ -> flat_cons step (flatten_sequence m seq)
| Have p | Type p | When p | Core p | Init p ->
begin
match F.is_ptrue p with
@@ -661,7 +669,7 @@ let rec flatten_sequence m = function
let sa = a.seq_list in
let sb = b.seq_list in
match a.seq_catg , b.seq_catg with
- | (TRUE|EMPTY) , (TRUE|EMPTY) ->
+ | (TRUE|KEEP) , (TRUE|KEEP) ->
m := true ; flatten_sequence m seq
| _ , FALSE ->
m := true ;
@@ -698,6 +706,7 @@ let rec flatten_sequence m = function
(* -------------------------------------------------------------------------- *)
let rec map_condition f = function
+ | Probe(p,t) -> Probe(p,F.p_lift f t)
| State s -> State (Mstate.apply (F.p_lift f) s)
| Have p -> Have (f p)
| Type p -> Type (f p)
@@ -730,6 +739,7 @@ module Ground = Letify.Ground
let rec ground_flow ~fwd env h =
match h.condition with
+ | Probe(p,t) -> update_cond h (Probe (p,Ground.e_apply env t))
| State s ->
let s = Mstate.apply (Ground.e_apply env) s in
update_cond h (State s)
@@ -743,8 +753,7 @@ let rec ground_flow ~fwd env h =
let b = ground_flowseq ~fwd wb b in
update_cond h (Branch(p,a,b))
| Either ws ->
- let ws = List.map
- (fun w -> ground_flowseq ~fwd (Ground.copy env) w) ws in
+ let ws = List.map (fun w -> ground_flowseq ~fwd (Ground.copy env) w) ws in
update_cond h (Either ws)
and ground_flowseq ~fwd env hs =
@@ -798,14 +807,14 @@ let dseq_of_step sigma step =
let defs =
match step.condition with
| Init p | Have p | When p | Core p -> Defs.extract (Sigma.p_apply sigma p)
- | Type _ | Branch _ | Either _ | State _ -> Defs.empty
+ | Type _ | Branch _ | Either _ | State _ | Probe _ -> Defs.empty
in defs , step
let letify_assume sref (_,step) =
let current = !sref in
begin
match step.condition with
- | Type _ | Branch _ | Either _ | State _ -> ()
+ | Type _ | Branch _ | Either _ | State _ | Probe _ -> ()
| Init p | Have p | When p | Core p ->
if Wp_parameters.Simpl.get () then
sref := Sigma.assume current p
@@ -842,6 +851,7 @@ let rec letify_seq sigma0 ~target ~export (seq : step list) =
and letify_step dseq dsigma ~required ~target ~used i (d,s) =
let sigma = dsigma.(i) in
let cond = match s.condition with
+ | Probe(p,t) -> Probe (p,Sigma.e_apply sigma t)
| State s -> State (Mstate.apply (Sigma.e_apply sigma) s)
| Init p ->
let p = Sigma.p_apply sigma p in
@@ -923,6 +933,7 @@ let apply_hyp modified solvers h =
| _ -> weaken_and_then_assume p
in
match h.condition with
+ | Probe(p,t) -> update_cond h (Probe (p,equivalent_exp solvers t))
| State s -> update_cond h (State (Mstate.apply (equivalent_exp solvers) s))
| Init p -> update_cond h (Init (weaken p))
| Type p -> update_cond h (Type (weaken p))
@@ -982,7 +993,7 @@ let empty = {
seq_size = 0 ;
seq_vars = Vars.empty ;
seq_core = Pset.empty ;
- seq_catg = EMPTY ;
+ seq_catg = TRUE ;
seq_list = [] ;
}
@@ -1016,10 +1027,19 @@ let seq_branch ?stmt p sa sb =
(* --- Introduction Utilities --- *)
(* -------------------------------------------------------------------------- *)
-let lemma g =
+let lemma ~loc g =
let cc g =
let hs,p = forall_intro g in
let hs = List.map (fun p -> step (Have p)) hs in
+ let hs =
+ if Wp_parameters.CounterExamples.get () then
+ let freevars = Vars.union (vars_list hs) (F.varsp p) in
+ List.fold_right
+ (fun x hs ->
+ let p = Probe.create ~loc ~name:(Var.basename x) () in
+ step (Probe(p,e_var x)) :: hs
+ ) (Vars.elements freevars) hs
+ else hs in
sequence hs , p
in Lang.local ~vars:(F.varsp g) cc g
@@ -1090,7 +1110,7 @@ struct
let collect s = function
| Have p | When p | Core p | Init p -> collect_set_def s (F.e_prop p)
- | Type _ | Branch _ | Either _ | State _ -> ()
+ | Type _ | Branch _ | Either _ | State _ | Probe _ -> ()
let subst s =
match s.cache with
@@ -1104,6 +1124,7 @@ struct
let p_apply s p = F.p_subst (subst s) p
let rec c_apply s = function
+ | Probe(p,t) -> Probe (p,e_apply s t)
| State m -> State (Mstate.apply (e_apply s) m)
| Type p -> Type (p_apply s p)
| Init p -> Init (p_apply s p)
@@ -1214,7 +1235,7 @@ let rec test_cases (s : hsp) = function
| Some _ , Some _ -> test_cases s tail
let rec collect_cond m = function
- | When _ | Have _ | Type _ | Init _ | Core _ | State _ -> ()
+ | When _ | Have _ | Type _ | Init _ | Core _ | State _ | Probe _ -> ()
| Branch(p,a,b) -> Letify.Split.add m p ; collect_seq m a ; collect_seq m b
| Either cs -> List.iter (collect_seq m) cs
@@ -1247,6 +1268,7 @@ let pruning ?(solvers=[]) seq =
let rec collect_cond u = function
| State _ -> ()
+ | Probe(_,t) -> Cleaning.as_term u t
| When p -> Cleaning.as_have u p
| Have p -> Cleaning.as_have u p
| Core p -> Cleaning.as_have u p
@@ -1259,7 +1281,7 @@ and collect_steps u steps =
List.iter (fun s -> collect_cond u s.condition) steps
let rec clean_cond u = function
- | State _ as cond -> cond
+ | State _ | Probe _ as cond -> cond
| When p -> When (Cleaning.filter_pred u p)
| Have p -> Have (Cleaning.filter_pred u p)
| Core p -> Core (Cleaning.filter_pred u p)
@@ -1282,9 +1304,9 @@ and clean_steps u = function
let c = clean_cond u s.condition in
let seq = clean_steps u seq in
match catg_cond c with
- | EMPTY -> seq
+ | TRUE -> seq
| FALSE -> [update_cond s c]
- | TRUE | MAYBE -> update_cond s c :: seq
+ | KEEP | MAYBE -> update_cond s c :: seq
let clean (s,p) =
let u = Cleaning.create () in
@@ -1416,6 +1438,12 @@ struct
Fset.empty
in m.footcalls <- Gmap.add f fs m.footcalls ; fs
+ let collect_term m t =
+ begin
+ m.gs <- FP.union m.gs (gvars_of_term ~deep:true m t) ;
+ m.xs <- Vars.union m.xs (F.vars t) ;
+ end
+
let collect_have m p =
begin
m.gs <- FP.union m.gs (gvars_of_pred ~deep:true m p) ;
@@ -1423,6 +1451,7 @@ struct
end
let rec collect_condition m = function
+ | Probe(_,t) -> collect_term m t
| Have p | When p | Core p -> collect_have m p
| Type _ | Init _ | State _ -> ()
| Branch(p,sa,sb) -> collect_have m p ; collect_seq m sa ; collect_seq m sb
@@ -1449,7 +1478,7 @@ struct
| [] -> []
| s :: w ->
match s.condition with
- | State _ | Have _ | When _ | Core _ | Branch _ | Either _ ->
+ | State _ | Probe _ | Have _ | When _ | Core _ | Branch _ | Either _ ->
s :: filter_steplist m w
| Type p ->
let p = filter_pred m p in
@@ -1602,6 +1631,7 @@ struct
let rec collect_step w s =
match s.condition with
| Type _ | State _ -> w
+ | Probe(_,t) -> usage w t
| Have p | Core p | Init p | When p -> usage w (F.e_prop p)
| Branch(p,a,b) ->
let wa = collect_seq w a in
@@ -1639,7 +1669,7 @@ struct
let rec collect_step filter s =
match s.condition with
| State s -> add_state filter s
- | Have _ | Core _ | Init _ | When _ | Type _ -> filter
+ | Have _ | Core _ | Init _ | When _ | Type _ | Probe _ -> filter
| Branch(_p,a,b) -> collect_seq (collect_seq filter a) b
| Either ws -> List.fold_left collect_seq filter ws
@@ -1699,18 +1729,17 @@ let alter_closure sequent = List.fold_left (fun seq f -> f seq) sequent !closure
let hyps s = List.map (fun s -> close_cond s.condition) s.seq_list
let head s =
match s.condition with
- | Have p | When p | Core p | Init p | Type p
- | Branch(p,_,_) -> p
- | Either _ | State _ -> p_true
+ | Have p | When p | Core p | Init p | Type p | Branch(p,_,_) -> p
+ | Either _ | State _ | Probe _ -> p_true
let have s =
match s.condition with
| Have p | When p | Core p | Init p | Type p -> p
- | Branch _ | Either _ | State _ -> p_true
+ | Branch _ | Either _ | State _ | Probe _ -> p_true
let condition s = F.p_conj (hyps s)
-let close sequent =
+let property sequent =
let s,goal = alter_closure sequent in
- F.p_close (F.p_hyps (hyps s) goal)
+ (F.p_hyps (hyps s) goal)
(* -------------------------------------------------------------------------- *)
(* --- Visitor --- *)
@@ -1719,6 +1748,21 @@ let close sequent =
let list seq = seq.seq_list
let iter f seq = List.iter f seq.seq_list
+(* -------------------------------------------------------------------------- *)
+(* --- Probes --- *)
+(* -------------------------------------------------------------------------- *)
+
+let probes seq =
+ let pool = ref Probe.Map.empty in
+ let rec collect_step s =
+ match s.condition with
+ | Probe(p,t) -> pool := Probe.Map.add p t !pool
+ | Branch(_,a,b) -> collect_seq a ; collect_seq b
+ | Either cs -> List.iter collect_seq cs
+ | _ -> ()
+ and collect_seq s = List.iter collect_step s.seq_list
+ in collect_seq seq ; !pool
+
(* -------------------------------------------------------------------------- *)
(* --- Index --- *)
(* -------------------------------------------------------------------------- *)
@@ -1730,7 +1774,7 @@ let rec index_list k = function
and index_step k s =
s.id <- k ; let k = succ k in
match s.condition with
- | Have _ | When _ | Type _ | Core _ | Init _ | State _ -> k
+ | Have _ | When _ | Type _ | Core _ | Init _ | State _ | Probe _ -> k
| Branch(_,a,b) -> index_list (index_list k a.seq_list) b.seq_list
| Either cs -> index_case k cs
@@ -1754,7 +1798,8 @@ let rec at_list k = function
if k < n then at_step (k-1) s.condition else at_list (k - n) w
and at_step k = function
- | Have _ | When _ | Type _ | Core _ | Init _ | State _ -> assert false
+ | Have _ | When _ | Type _ | Core _ | Init _ | State _ | Probe _ ->
+ assert false
| Branch(_,a,b) ->
let n = a.seq_size in
if k < n then
@@ -1798,7 +1843,8 @@ let in_sequence_add_list ~replace =
else s :: in_list (k-n) h w
and in_step k h = function
- | Have _ | When _ | Type _ | Core _ | Init _ | State _ -> assert false
+ | Have _ | When _ | Type _ | Core _ | Init _ | State _ | Probe _ ->
+ assert false
| Branch(p,a,b) ->
let n = a.seq_size in
if k < n then
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 8194fdef251323169ef6efa15c89e39d777e00bf..4f314f0ac7168d74110139900a53a246f197d994 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -62,6 +62,7 @@ and condition =
| Branch of pred * sequence * sequence (** If-Then-Else *)
| Either of sequence list (** Disjunction *)
| State of Mstate.state (** Memory Model snapshot *)
+ | Probe of Probe.t * term (** Named probes *)
and sequence (** List of steps *)
@@ -143,6 +144,9 @@ val step_at : sequence -> int -> step
val is_trivial : sequent -> bool
(** Goal is true or hypotheses contains false. *)
+val probes : sequence -> term Probe.Map.t
+(** Collect all probes in the sequence *)
+
(** {2 Transformations} *)
val map_condition : (pred -> pred) -> condition -> condition
@@ -184,7 +188,7 @@ val introduction : sequent -> sequent option
val introduction_eq : sequent -> sequent
(** Same as [introduction] but returns the same sequent is None *)
-val lemma : pred -> sequent
+val lemma : loc:location -> pred -> sequent
(** Performs existential, universal and hypotheses introductions *)
val head : step -> pred
@@ -198,8 +202,8 @@ val pred_cond : condition -> pred
val condition : sequence -> pred
(** With free variables kept. *)
-val close : sequent -> pred
-(** With free variables {i quantified}. *)
+val property : sequent -> pred
+(** With free variables kept. *)
val at_closure : (sequent -> sequent ) -> unit
(** register a transformation applied just before close *)
@@ -235,6 +239,10 @@ val merge : bundle list -> bundle
Linear complexity is achieved by assuming bundle ordering is consistent
over the list. *)
+(** Inserts probes to a sequent. *)
+val probe : loc:location -> ?descr:string -> ?stmt:stmt -> name:string ->
+ term -> bundle -> bundle
+
(** Assumes a list of predicates in a [Type] section on top of the bundle. *)
val domain : F.pred list -> bundle -> bundle
diff --git a/src/plugins/wp/Filtering.ml b/src/plugins/wp/Filtering.ml
index 802135e7cdd30d6fe358f5d87b9f182d1de4aeec..a586f8820eb613fa0eeb946924d308f880c69a5e 100644
--- a/src/plugins/wp/Filtering.ml
+++ b/src/plugins/wp/Filtering.ml
@@ -272,23 +272,29 @@ struct
mutable target : domain ;
}
+ let collect_term env t =
+ let dp = Value.domain env.usage t in
+ if not (Domain.separated dp env.target)
+ then env.target <- Domain.join dp env.target
+
+ let collect_probe env t =
+ let dp = Value.domain env.usage t in
+ env.target <- Domain.join dp env.target
+
let rec collect_hyp env p =
match F.p_expr p with
| And ps | Or ps -> List.iter (collect_hyp env) ps
| Imply(hs,p) ->
List.iter (collect_hyp env) hs ;
collect_hyp env p
- | _ ->
- let dp = Value.domain env.usage (F.e_prop p) in
- if not (Domain.separated dp env.target)
- then
- ( env.target <- Domain.join dp env.target )
+ | _ -> collect_term env (F.e_prop p)
let rec collect_seq env s = Conditions.iter (collect_step env) s
and collect_step env s =
let open Conditions in
match s.condition with
| Type _ | State _ -> ()
+ | Probe(_,t) -> collect_probe env t
| Core p | Have p | When p | Init p -> collect_hyp env p
| Either cs -> List.iter (collect_seq env) cs
| Branch(p,a,b) ->
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 8d066e1cca6f7e1aedb0058f9b54562d167612ae..399a5abea2e8384b3fda22a6358e30a2e1405b1a 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -808,7 +808,7 @@ struct
let define_lemma c l =
if l.lem_labels <> [] && Wp_parameters.has_dkey dkey_lemma then
- Wp_parameters.warning ~source:l.lem_position
+ Wp_parameters.warning ~source:(fst l.lem_loc)
"Lemma '%s' has labels, consider using global invariant instead."
l.lem_name ;
let { tp_kind = kind ; tp_statement = p } = l.lem_predicate in
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index 6293ff03d718e6bfe78f51c7e0eeb8fb4aafcaac..800f68faa67d635fa88e182fec42cf387307e25c 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -58,8 +58,8 @@ let trim name =
(* -------------------------------------------------------------------------- *)
type logic_lemma = {
+ lem_loc : location ;
lem_name : string ;
- lem_position : Filepath.position ;
lem_types : string list ;
lem_labels : logic_label list ;
lem_predicate : toplevel_predicate ;
@@ -193,7 +193,7 @@ let pp_profile fmt l =
let ip_lemma l =
Property.ip_lemma {
il_name = l.lem_name; il_labels = l.lem_labels;
- il_args = l.lem_types; il_loc = (l.lem_position, l.lem_position);
+ il_args = l.lem_types; il_loc = l.lem_loc;
il_attrs = l.lem_attrs;
il_pred = l.lem_predicate;
}
@@ -201,8 +201,8 @@ let ip_lemma l =
let lemma_of_global ~context = function
| Dlemma(name,labels,types,pred,attrs,loc) ->
{
+ lem_loc = loc ;
lem_name = name ;
- lem_position = fst loc ;
lem_types = types ;
lem_labels = labels ;
lem_predicate = pred ;
diff --git a/src/plugins/wp/LogicUsage.mli b/src/plugins/wp/LogicUsage.mli
index 51428deaf89b1c8ed968fbac37b27c329127e90a..2650640095fe937c099623de24805889641630b0 100644
--- a/src/plugins/wp/LogicUsage.mli
+++ b/src/plugins/wp/LogicUsage.mli
@@ -31,8 +31,8 @@ open Clabels
val basename : varinfo -> string (** Trims the original name *)
type logic_lemma = {
+ lem_loc : location ;
lem_name : string ;
- lem_position : Filepath.position ;
lem_types : string list ;
lem_labels : logic_label list ;
lem_predicate : toplevel_predicate ;
diff --git a/src/plugins/wp/Pattern.ml b/src/plugins/wp/Pattern.ml
index 71ad146b74e37e7db1837e3173ca3a30b659a97b..c0660c931eb529f218cdeb03ab8c3efdefd1d641 100644
--- a/src/plugins/wp/Pattern.ml
+++ b/src/plugins/wp/Pattern.ml
@@ -498,12 +498,13 @@ let order (s : Conditions.step) : int =
| Type _ -> 5
| Either _ -> 6
| State _ -> 7
+ | Probe _ -> 8
let priority sa sb = order sa - order sb
let push (step : Conditions.step) =
match step.condition with
- | Have _ | When _ | Core _ | Init _ | Type _ | State _ -> ()
+ | Have _ | When _ | Core _ | Init _ | Type _ | State _ | Probe _ -> ()
| Branch(_,sa,sb) -> Queue.push sa queue ; Queue.push sb queue
| Either cs -> List.iter (fun s -> Queue.push s queue) cs
diff --git a/src/plugins/wp/Pcfg.ml b/src/plugins/wp/Pcfg.ml
index aeefb7a4664a5ae6750b2978b2a6a5d546b5289f..69d0ca8243784104d50ae8ab820a4ce27d419197 100644
--- a/src/plugins/wp/Pcfg.ml
+++ b/src/plugins/wp/Pcfg.ml
@@ -144,7 +144,7 @@ and ctrl env prev steps next = match steps with
| s :: others ->
let open Conditions in
match s.condition with
- | Type _ | Have _ | When _ | Core _ | Init _ ->
+ | Type _ | Have _ | When _ | Core _ | Init _ | Probe _ ->
(* Sequence of Labels on Hyp *)
ctrl env prev others next
| Branch(_,cthen,celse) ->
@@ -187,7 +187,7 @@ let register seq =
| { id ; stmt ; descr ; condition = State m } ->
let label = label env ~id ?stmt ?descr m in
let r = pool descr in r := label :: !r
- | { condition = Type _ | Have _ | When _ | Core _ | Init _ } -> ()
+ | { condition = Type _ | Have _ | When _ | Core _ | Init _ | Probe _ } -> ()
| { condition = Branch(_,cthen,celse) } -> push cthen ; push celse
| { condition = Either cases } -> List.iter push cases
) seq ;
diff --git a/src/plugins/wp/Pcond.ml b/src/plugins/wp/Pcond.ml
index 26c32cbfdacecbe9f5bdc1abdf3bf6756a649831..471a236cd943c599d6ebf3ee6f2f9381bab1d560 100644
--- a/src/plugins/wp/Pcond.ml
+++ b/src/plugins/wp/Pcond.ml
@@ -37,7 +37,7 @@ let rec alloc_hyp pool f seq =
(fun step ->
if not (Vars.subset step.vars (Plang.alloc_domain pool)) then
match step.condition with
- | State _ ->
+ | State _ | Probe _ ->
Plang.alloc_xs pool f step.vars
| Have p | When p | Type p | Init p | Core p ->
Plang.alloc_p pool f p
@@ -179,8 +179,8 @@ open Conditions
let mark_step m step =
(* sub-sequences are marked recursively marked later *)
match step.condition with
- | When p | Type p | Have p | Init p | Core p
- | Branch(p,_,_) -> F.mark_p m p
+ | When p | Type p | Have p | Init p | Core p | Branch(p,_,_) -> F.mark_p m p
+ | Probe(_,t) -> F.mark_e m t
| Either _ | State _ -> ()
let spaced pp fmt a = Format.pp_print_space fmt () ; pp fmt a
@@ -215,28 +215,35 @@ class engine (lang : #Plang.engine) =
Format.fprintf fmt "@[<hov 4>%a %a = %a.@]"
self#pp_clause "Let" self#pp_name x self#pp_core e
- method pp_intro ~step ~clause ?(dot=".") fmt p =
- ignore step ;
+ method pp_intro ~clause ?(dot=".") fmt p =
Format.fprintf fmt "@[<hov 4>%a %a%s@]"
self#pp_clause clause lang#pp_pred p dot
+ method pp_probe fmt p t =
+ begin
+ Format.fprintf fmt "@[<hov 4>%a %a = %a.@]"
+ self#pp_clause "Probe" Probe.pretty p lang#pp_term t
+ end
+
(* -------------------------------------------------------------------------- *)
(* --- Block Printers --- *)
(* -------------------------------------------------------------------------- *)
- method pp_condition ~step fmt = function
+ method pp_condition fmt step =
+ match step.condition with
| State _ -> ()
- | Core p -> self#pp_intro ~step ~clause:"Core:" fmt p
- | Type p -> self#pp_intro ~step ~clause:"Type:" fmt p
- | Init p -> self#pp_intro ~step ~clause:"Init:" fmt p
- | Have p -> self#pp_intro ~step ~clause:"Have:" fmt p
- | When p -> self#pp_intro ~step ~clause:"When:" fmt p
+ | Probe(p,t) -> self#pp_probe fmt p t
+ | Core p -> self#pp_intro ~clause:"Core:" fmt p
+ | Type p -> self#pp_intro ~clause:"Type:" fmt p
+ | Init p -> self#pp_intro ~clause:"Init:" fmt p
+ | Have p -> self#pp_intro ~clause:"Have:" fmt p
+ | When p -> self#pp_intro ~clause:"When:" fmt p
| Branch(p,sa,sb) ->
begin
- self#pp_intro ~step ~clause:"If" ~dot:"" fmt p ;
- if not (Conditions.is_true sa)
+ self#pp_intro ~clause:"If" ~dot:"" fmt p ;
+ if not (Conditions.is_empty sa)
then self#sequence ~clause:"Then" fmt sa ;
- if not (Conditions.is_true sb)
+ if not (Conditions.is_empty sb)
then self#sequence ~clause:"Else" fmt sb ;
end
| Either cases ->
@@ -253,21 +260,21 @@ class engine (lang : #Plang.engine) =
method pp_step fmt step =
match step.condition with
- | State _ ->
- self#pp_condition ~step fmt step.condition
+ | State _ -> self#pp_condition fmt step
| _ ->
begin
( match step.descr with None -> () | Some s ->
spaced self#pp_comment fmt s ) ;
Warning.Set.iter (spaced self#pp_warning fmt) step.warn ;
List.iter (spaced self#pp_property fmt) step.deps ;
- spaced (self#pp_condition ~step) fmt step.condition ;
+ spaced self#pp_condition fmt step ;
end
method private sequence ~clause fmt seq =
Format.pp_print_space fmt () ; self#pp_block ~clause fmt seq
+
method pp_block ~clause fmt seq =
- if Conditions.is_true seq then
+ if Conditions.is_empty seq then
Format.fprintf fmt "%a {}" self#pp_clause clause
else
begin
@@ -286,7 +293,7 @@ class engine (lang : #Plang.engine) =
Format.fprintf fmt "@[<hv 0>" ;
List.iter (append (self#define env) fmt) (F.defs marks) ;
lang#set_env env ;
- if not (Conditions.is_true hs) then
+ if not (Conditions.is_empty hs) then
begin
self#pp_block ~clause:"Assume" fmt hs ;
Format.pp_print_newline fmt () ;
@@ -337,7 +344,8 @@ class seqengine (lang : #state) =
object(self)
inherit engine lang as super
- method private label step = function
+ method private label step =
+ match step.condition with
| State _ ->
(try Some (lang#label_at ~id:step.id)
with Not_found -> None)
@@ -349,9 +357,9 @@ class seqengine (lang : #state) =
if not (Bag.is_empty upd) then
Bag.iter ((spaced (lang#pp_update lbl)) fmt) upd
- method! pp_condition ~step fmt cond =
- match self#label step cond with
- | None -> super#pp_condition ~step fmt cond
+ method! pp_condition fmt step =
+ match self#label step with
+ | None -> super#pp_condition fmt step
| Some lbl ->
let before = match Pcfg.prev lbl with
| [ pre ] when (Pcfg.branching pre) ->
diff --git a/src/plugins/wp/Pcond.mli b/src/plugins/wp/Pcond.mli
index ce7ef09ff46a0c1f800632ec0a1f350494456e77..ef53b285566e780682d0121e3d9c2fe5710d8b3f 100644
--- a/src/plugins/wp/Pcond.mli
+++ b/src/plugins/wp/Pcond.mli
@@ -79,8 +79,9 @@ class engine : #Plang.engine ->
(** Default: [plang#pp_sort] *)
method pp_definition : Format.formatter -> string -> term -> unit
- method pp_intro : step:step -> clause:string -> ?dot:string -> pred printer
- method pp_condition : step:step -> condition printer
+ method pp_intro : clause:string -> ?dot:string -> pred printer
+ method pp_probe : Format.formatter -> Probe.t -> term -> unit
+ method pp_condition : step printer
method pp_block : clause:string -> sequence printer
method pp_goal : pred printer
diff --git a/src/plugins/wp/Probe.ml b/src/plugins/wp/Probe.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9c5aa89d7e394125da5c04857dc7330717a4c5f3
--- /dev/null
+++ b/src/plugins/wp/Probe.ml
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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 Cil_types
+
+(* -------------------------------------------------------------------------- *)
+(* --- User-Defined Probes --- *)
+(* -------------------------------------------------------------------------- *)
+
+type probe = {
+ id : int;
+ name : string ;
+ stmt : stmt option ;
+ loc : location ;
+}
+
+let create =
+ let id = ref (-1) in
+ fun ~loc ?stmt ~name () ->
+ incr id; { id = !id ; loc ; stmt ; name }
+
+module S =
+struct
+ include Datatype.Undefined
+ let name = "WP.Conditions.Probe.t"
+ let reprs = [{
+ loc = Cil_datatype.Location.unknown; stmt = None; name = ""; id=1
+ }]
+ type t = probe
+ let hash x = x.id
+ let equal x y = Int.equal x.id y.id
+ let compare x y = Int.compare y.id x.id (* lastly created first (wp) *)
+ let pretty fmt p =
+ if Wp_parameters.debug_atleast 1 then
+ Format.fprintf fmt "%s#%d" p.name p.id
+ else
+ Format.fprintf fmt "%s" p.name
+end
+
+include Datatype.Make_with_collections(S)
+
+(* -------------------------------------------------------------------------- *)
+(* --- ACSL Extension --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec name_of_host = function
+ | TVar { lv_name = x } -> x
+ | TResult _ -> "result" (* currently not used, but could be one day *)
+ | TMem t -> name_of_term t
+
+and name_of_term (t : term) =
+ match t.term_name with a::_ -> a | _ ->
+ match t.term_node with
+ | TLval (lh,_) | TAddrOf (lh,_) | TStartOf (lh,_) -> name_of_host lh
+ | _ -> raise Not_found
+
+let annotations stmt =
+ let collect _emitter annot acc =
+ match annot.annot_content with
+ | Cil_types.AExtended (_, _, {
+ ext_name="probe" ;
+ ext_kind=Ext_terms ps ;
+ }) -> List.rev_append ps acc
+ | _ -> acc in
+ let mk_probe t =
+ try name_of_term t, t
+ with Not_found ->
+ Wp_parameters.abort ~source:(fst t.term_loc)
+ "Missing name for probe, use @probe A: term;"
+ in List.rev_map mk_probe (Annotations.fold_code_annot collect stmt [])
+
+let parse_probe : Acsl_extension.extension_typer =
+ fun context _loc terms ->
+ (* use default context of the code-annotation (like an assert clause) *)
+ let parse_term = context.type_term context context.pre_state in
+ Ext_terms (List.map parse_term terms)
+
+let registered = ref false
+let register () =
+ if not !registered && Wp_parameters.Probes.get () then
+ begin
+ registered := true ;
+ Acsl_extension.register_code_annot "probe" parse_probe false ;
+ end
+
+let () = Cmdline.run_after_configuring_stage register
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Probe.mli b/src/plugins/wp/Probe.mli
new file mode 100644
index 0000000000000000000000000000000000000000..068dc0fa24d87d3b1a6f80490bccb2b2092729fc
--- /dev/null
+++ b/src/plugins/wp/Probe.mli
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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 Cil_types
+
+type probe = private {
+ id : int;
+ name : string ;
+ stmt : stmt option ;
+ loc : location ;
+}
+
+val annotations : stmt -> (string * term) list
+val create : loc:location -> ?stmt:stmt -> name:string -> unit -> probe
+
+include Datatype.S_with_collections with type t = probe
+
+(**************************************************************************)
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index c8d5ede112bf3b6ba8c6d806b31b952f2d358f9d..da270ebd1d85c68271d689e33e8358c975191e5d 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -49,6 +49,7 @@ let s_kind s = match s.condition with
| Type _ -> "type"
| Init _ -> "init"
| Branch _ -> "branch"
+ | Probe _ -> "probe"
| Either _ -> "either"
| State _ -> "state"
@@ -337,6 +338,7 @@ let json_of_verdict = function
| VCS.Timeout -> `String "timeout"
| VCS.Stepout -> `String "stepout"
| VCS.Failed -> `String "failed"
+ | VCS.Invalid -> `String "invalid"
let verdict_of_json = function
| `String "valid" -> VCS.Valid
@@ -344,6 +346,7 @@ let verdict_of_json = function
| `String "timeout" -> VCS.Timeout
| `String "stepout" -> VCS.Stepout
| `String "failed" -> VCS.Failed
+ | `String "invalid" -> VCS.Invalid
| _ -> VCS.NoResult
let json_of_result (p : VCS.prover) (r : VCS.result) =
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index cde11bcadfec61eb768eeef08cb95aedbf969800..b97a388f6c93f06d8676f31e71270a5c3c1183b2 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -23,6 +23,7 @@
let dkey = Wp_parameters.register_category "prover"
let dkey_pp_task = Wp_parameters.register_category "prover:pp_task"
let dkey_api = Wp_parameters.register_category "why3_api"
+let dkey_model = Wp_parameters.register_category "why3_model"
let option_file = LogicBuiltins.create_option
~sanitizer:(fun ~driver_dir x -> Filename.concat driver_dir x)
@@ -348,14 +349,16 @@ let rec of_trigger ~cnv t =
end
let rec of_term ~cnv expected t : Why3.Term.term =
- Wp_parameters.debug ~dkey:dkey_api
- "of_term %a %a@."
- Lang.F.Tau.pretty expected Lang.F.pp_term t;
let sort =
try Lang.F.typeof t
with Not_found ->
why3_failure "@[<hov 2>Untyped term: %a@]" Lang.F.pp_term t
in
+ Wp_parameters.debug ~dkey:dkey_api
+ "of_term %a:%a (expected %a)@."
+ Lang.F.pp_term t Lang.F.Tau.pretty sort Lang.F.Tau.pretty expected
+ ;
+
let ($) f x = f x in
let r =
try coerce ~cnv sort expected $ Lang.F.Tmap.find t cnv.subst
@@ -634,8 +637,7 @@ and share cnv expected t =
let t = List.fold_left (fun t (x,e') ->
Why3.Term.t_let_close x e' t
) t lets
- in
- t
+ in t
and mk_lets cnv l =
List.fold_left (fun (cnv,lets) e ->
@@ -647,9 +649,9 @@ and mk_lets cnv l =
let x = Why3.Ident.id_fresh (Lang.F.basename e) in
let x = Why3.Term.create_vsymbol x ty in
(* Format.printf "lets %a = %a : %a@."
- * Why3.Pretty.print_vsty x
- * Why3.Pretty.print_term e'
- * Why3.Pretty.print_ty (Why3.Term.t_type e'); *)
+ Why3.Pretty.print_vsty x
+ Why3.Pretty.print_term e'
+ Why3.Pretty.print_ty (Why3.Term.t_type e'); *)
let cnv = {cnv with subst = Lang.F.Tmap.add e (Why3.Term.t_var x) cnv.subst } in
let lets = (x,e')::lets in
cnv,lets
@@ -676,11 +678,13 @@ and int_or_real ~cnv ~fint ~lint ~pint ~freal ~lreal ~preal a b =
t_app_fold ~f:freal ~l:lreal ~p:preal ~cnv Real [a; b]
| _ -> assert false
+let rebuild cnv t =
+ let t, cache = Lang.For_export.rebuild ~cache:cnv.convert_for_export t in
+ cnv.convert_for_export <- cache;
+ t
+
let convert cnv expected t =
- (* rewrite terms which normal form inside qed are different from the one of the provers *)
- let t, convert_for_export = Lang.For_export.rebuild ~cache:cnv.convert_for_export t in
- cnv.convert_for_export <- convert_for_export;
- Lang.For_export.in_state (share cnv expected) t
+ Lang.For_export.in_state (share cnv expected) (rebuild cnv t)
let mk_binders cnv l =
List.fold_left (fun (cnv,lets) v ->
@@ -689,8 +693,9 @@ let mk_binders cnv l =
| Some ty ->
let x = Why3.Ident.id_fresh (Lang.F.Var.basename v) in
let x = Why3.Term.create_vsymbol x ty in
- let e = Lang.F.e_var v in
- let cnv = {cnv with subst = Lang.F.Tmap.add e (Why3.Term.t_var x) cnv.subst } in
+ let ex = Lang.F.e_var v in
+ let tx = Why3.Term.t_var x in
+ let cnv = { cnv with subst = Lang.F.Tmap.add ex tx cnv.subst } in
let lets = x::lets in
cnv,lets
) (cnv,[]) (List.rev l)
@@ -1068,7 +1073,48 @@ class visitor (ctx:context) c =
let goal_id = (Why3.Decl.create_prsymbol (Why3.Ident.id_fresh "wp_goal"))
-let prove_goal ~id ~title ~name ?axioms t =
+let add_model_trace (probes: Lang.F.term Probe.Map.t) cnv t =
+ let open Why3 in
+ if Probe.Map.is_empty probes then t else
+ let task = Task.add_meta t Driver.meta_get_counterexmp [Theory.MAstr ""] in
+ let create_id (p:Probe.t) ty =
+ let attr = Ident.create_model_trace_attr (string_of_int p.id) in
+ let attrs = Ident.Sattr.singleton attr in
+ let loc = match p.loc with
+ ({Filepath.pos_path;pos_lnum=l1;pos_cnum=c1},
+ {Filepath.pos_lnum=l2;pos_cnum=c2}) ->
+ Why3.Loc.user_position
+ (Filepath.Normalized.to_pretty_string pos_path) l1 c1 l2 c2
+ in Term.create_lsymbol (Ident.id_fresh ~loc ~attrs p.name) [] ty
+ in
+ let fold (p:Probe.t) (term:Lang.F.term) task =
+ let term' = share cnv (Lang.F.typeof term) term in
+ let id = create_id p term'.t_ty in
+ let task = Task.add_param_decl task id in
+ let eq_id = Why3.Decl.create_prsymbol (Why3.Ident.id_fresh "ce_eq") in
+ let eq = Term.t_equ (Term.t_app id [] term'.t_ty) term' in
+ let decl = Why3.Decl.create_prop_decl Paxiom eq_id eq in
+ Task.add_decl task decl
+ in
+ Probe.Map.fold fold probes task
+
+let convert_freevariables ~probes ~cnv t =
+ let freevars = Probe.Map.fold
+ (fun _ t vars -> Lang.F.Vars.union vars (Lang.F.vars t))
+ probes (Lang.F.vars t) in
+ let cnv,lss =
+ Lang.F.Vars.fold (fun (v:Lang.F.Var.t) (cnv,lss) ->
+ let ty = of_tau ~cnv @@ Lang.F.tau_of_var v in
+ let x = Why3.Ident.id_fresh (Lang.F.Var.basename v) in
+ let ls = Why3.Term.create_lsymbol x [] ty in
+ let ex = Lang.F.e_var v in
+ let tx = Why3.Term.t_app ls [] ty in
+ let cnv = { cnv with subst = Lang.F.Tmap.add ex tx cnv.subst } in
+ (cnv,ls::lss)) freevars (cnv,[])
+ in
+ cnv,lss
+
+let prove_goal ~id ~title ~name ?axioms ?(probes=Probe.Map.empty) t =
(* Format.printf "why3_of_qed start@."; *)
let goal = Definitions.cluster ~id ~title () in
let ctx = empty_context name in
@@ -1083,33 +1129,42 @@ let prove_goal ~id ~title ~name ?axioms t =
v#add_builtin_lib;
v#vgoal axioms t;
let cnv = empty_cnv ~polarity:`Positive ctx in
- let t = convert cnv Prop (Lang.F.e_prop t) in
- let decl = Why3.Decl.create_prop_decl Pgoal goal_id t in
- let th = Why3.Theory.close_theory ctx.th in
- if Wp_parameters.has_print_generated () then begin
- let th_uc_tmp = Why3.Theory.add_decl ~warn:false ctx.th decl in
- let th_tmp = Why3.Theory.close_theory th_uc_tmp in
- Wp_parameters.debug ~dkey:Wp_parameters.cat_print_generated "%a"
- Why3.Pretty.print_theory th_tmp
- end;
- th, decl
-
-let prove_prop ?axioms ~pid prop =
+ let t = rebuild cnv (Lang.F.e_prop t) in
+ let probes = Probe.Map.map (rebuild cnv) probes in
+ Lang.For_export.in_state
+ begin fun () ->
+ let cnv,lss = convert_freevariables ~probes ~cnv t in
+ let goal = share cnv Prop t in
+ let decl = Why3.Decl.create_prop_decl Pgoal goal_id goal in
+ let th = Why3.Theory.close_theory ctx.th in
+ if Wp_parameters.has_print_generated () then begin
+ let th_uc_tmp = Why3.Theory.add_decl ~warn:false ctx.th decl in
+ let th_tmp = Why3.Theory.close_theory th_uc_tmp in
+ Wp_parameters.debug ~dkey:Wp_parameters.cat_print_generated "%a"
+ Why3.Pretty.print_theory th_tmp
+ end;
+ let t = None in
+ let t = Why3.Task.use_export t th in
+ let t = List.fold_left Why3.Task.add_param_decl t lss in
+ let t = add_model_trace probes cnv t in
+ Why3.Task.add_decl t decl
+ end ()
+
+let prove_prop ?probes ?axioms ~pid prop =
let id = WpPropId.get_propid pid in
let title = Pretty_utils.to_string WpPropId.pretty pid in
let name = "WP" in
- let th, decl = prove_goal ?axioms ~id ~title ~name prop in
- let t = None in
- let t = Why3.Task.use_export t th in
- Why3.Task.add_decl t decl
+ prove_goal ?axioms ?probes ~id ~title ~name prop
-let task_of_wpo wpo =
+let compute_probes ~ce ~pid goal =
+ if ce then Wpo.GOAL.compute_probes ~pid goal else Probe.Map.empty
+
+let task_of_wpo ~ce wpo =
let v = wpo.Wpo.po_formula in
let pid = wpo.Wpo.po_pid in
- let axioms = v.Wpo.VC_Annot.axioms in
- let prop = Wpo.GOAL.compute_proof ~pid v.Wpo.VC_Annot.goal in
- (* Format.printf "Goal: %a@." Lang.F.pp_pred prop; *)
- prove_prop ~pid prop ?axioms
+ let prop = Wpo.GOAL.compute_proof ~pid ~opened:ce v.goal in
+ let probes = compute_probes ~ce ~pid v.goal in
+ prove_prop ~pid ?axioms:v.axioms ~probes prop, probes
(* -------------------------------------------------------------------------- *)
(* --- Prover Task --- *)
@@ -1153,7 +1208,50 @@ type prover_call = {
mutable killed : bool ;
}
-let ping_prover_call ~config p =
+let has_model_attr attrs =
+ Why3.Ident.Sattr.fold_left (fun acc (e:Why3.Ident.attribute) ->
+ match Extlib.string_del_prefix "model_trace:" e.attr_string with
+ | None -> acc
+ | Some _ as a -> a
+ ) None attrs
+
+let debug_model (res:Why3.Call_provers.prover_result) =
+ Wp_parameters.debug ~dkey:dkey_model "%t"
+ begin fun fmt ->
+ List.iter
+ begin fun (res,model) ->
+ Format.fprintf fmt "@[<hov 2>model %a: %a@]@\n"
+ Why3.Call_provers.print_prover_answer res
+ (Why3.Model_parser.print_model_human
+ ~filter_similar:false
+ ~print_attrs:true) model
+ end
+ res.pr_models
+ end
+
+let get_model probes (res:Why3.Call_provers.prover_result) =
+ if Wp_parameters.has_dkey dkey_model && not @@ Probe.Map.is_empty probes then
+ debug_model (res:Why3.Call_provers.prover_result);
+ (* we take the second model because it should be the most precise?? *)
+ match Why3.Check_ce.select_model_last_non_empty res.pr_models with
+ | None -> Probe.Map.empty
+ | Some model ->
+ let index = Hashtbl.create 0 in
+ let elements = Why3.Model_parser.get_model_elements model in
+ List.iter
+ (fun (e:Why3.Model_parser.model_element) ->
+ match has_model_attr e.me_attrs with
+ | None -> ()
+ | Some id -> Hashtbl.add index id e.me_concrete_value)
+ elements ;
+ Probe.Map.filter_map
+ (fun (p:Probe.t) _ ->
+ let id = string_of_int p.id in
+ try Some (Hashtbl.find index id)
+ with Not_found -> None
+ ) probes
+
+let ping_prover_call ~config ~probes p =
match Why3.Call_provers.query_call p.call with
| NoUpdates
| ProverStarted ->
@@ -1187,7 +1285,13 @@ let ping_prover_call ~config p =
| Valid -> VCS.result ~time ~steps:pr.pr_steps VCS.Valid
| OutOfMemory -> VCS.failed "out of memory"
| StepLimitExceeded -> VCS.result ?steps:p.steps VCS.Stepout
- | Unknown _ | Invalid -> VCS.unknown
+ | Invalid ->
+ debug_model pr;
+ VCS.result ~time:pr.pr_time ~steps:pr.pr_steps
+ ~model:(get_model probes pr) VCS.Invalid
+ | Unknown _ ->
+ debug_model pr;
+ VCS.result ~model:(get_model probes pr) VCS.Unknown
| _ when p.interrupted -> VCS.timeout p.timeout
| Failure s -> VCS.failed s
| HighFailure ->
@@ -1205,7 +1309,7 @@ let ping_prover_call ~config p =
VCS.pp_result r;
Task.Return (Task.Result r)
-let call_prover_task ~timeout ~steps ~config prover call =
+let call_prover_task ~timeout ~steps ~config ~probes prover call =
Wp_parameters.debug ~dkey "Why3 run prover %a with timeout %f, steps %d@."
Why3.Whyconf.print_prover prover
(Option.value ~default:(0.0) timeout)
@@ -1222,7 +1326,7 @@ let call_prover_task ~timeout ~steps ~config prover call =
pcall.killed <- true ;
Why3.Call_provers.interrupt_call ~config call ;
Task.Yield
- | Task.Coin -> ping_prover_call ~config pcall
+ | Task.Coin -> ping_prover_call ~config ~probes pcall
in
Task.async ping
@@ -1230,29 +1334,40 @@ let call_prover_task ~timeout ~steps ~config prover call =
(* --- Batch Prover --- *)
(* -------------------------------------------------------------------------- *)
+let output_task wpo drv ?(script : Filepath.Normalized.t option) prover task =
+ let file = Wpo.DISK.file_goal
+ ~pid:wpo.Wpo.po_pid
+ ~model:wpo.Wpo.po_model
+ ~prover:(VCS.Why3 prover) in
+ Command.print_file file
+ begin fun fmt ->
+ Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
+ (Why3Provers.ident_why3 prover) ;
+ let old = Option.map
+ (fun fscript ->
+ let hash = Digest.file fscript |> Digest.to_hex in
+ Format.fprintf fmt "(* WP Script %s *)@\n" hash ;
+ open_in fscript
+ ) (script :> string option) in
+ let _ = Why3.Driver.print_task_prepared ?old drv fmt task in
+ Option.iter close_in old ;
+ end
+
+
let digest_task wpo drv ?(script : Filepath.Normalized.t option) prover task =
+ output_task wpo drv ?script prover task;
let file = Wpo.DISK.file_goal
~pid:wpo.Wpo.po_pid
~model:wpo.Wpo.po_model
~prover:(VCS.Why3 prover) in
begin
- Command.print_file file
- begin fun fmt ->
- Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
- (Why3Provers.ident_why3 prover) ;
- let old = Option.map
- (fun fscript ->
- let hash = Digest.file fscript |> Digest.to_hex in
- Format.fprintf fmt "(* WP Script %s *)@\n" hash ;
- open_in fscript
- ) (script :> string option) in
- let _ = Why3.Driver.print_task_prepared ?old drv fmt task in
- Option.iter close_in old ;
- end ;
Digest.file (file :> string) |> Digest.to_hex
end
-let run_batch pconf driver ~config ?(script : Filepath.Normalized.t option) ~timeout ~steplimit ~memlimit
+let run_batch pconf driver ~config
+ ?(script : Filepath.Normalized.t option)
+ ~timeout ~steplimit ~memlimit
+ ?(probes=Probe.Map.empty)
prover task =
let steps = match steplimit with Some 0 -> None | _ -> steplimit in
let limit =
@@ -1277,9 +1392,10 @@ let run_batch pconf driver ~config ?(script : Filepath.Normalized.t option) ~tim
let command = Why3.Whyconf.get_complete_command pconf ~with_steps in
Wp_parameters.debug ~dkey "Prover command %S" command ;
let inplace = if script <> None then Some true else None in
- let call = Why3.Driver.prove_task_prepared ?old:(script :> string option) ?inplace
+ let call =
+ Why3.Driver.prove_task_prepared ?old:(script :> string option) ?inplace
~command ~limit ~config driver task in
- call_prover_task ~config ~timeout ~steps prover call
+ call_prover_task ~config ~timeout ~steps ~probes prover call
(* -------------------------------------------------------------------------- *)
(* --- Interactive Prover (Coq) --- *)
@@ -1321,14 +1437,14 @@ let editor ~script ~merge ~config pconf driver task =
if merge then updatescript ~script driver task ;
let command = editor_command pconf in
Wp_parameters.debug ~dkey "Editor command %S" command ;
- call_prover_task ~config ~timeout:None ~steps:None pconf.prover @@
+ let probes = Probe.Map.empty in
+ call_prover_task ~config ~timeout:None ~steps:None ~probes pconf.prover @@
Why3.Call_provers.call_editor ~command ~config (script :> string)
end
-let compile ~(script : Filepath.Normalized.t) ~timeout ~memlimit ~config wpo pconf driver prover task =
- let digest = digest_task wpo driver ~script in
- let runner = run_batch ~config pconf driver ~script ~memlimit in
- Cache.get_result ~digest ~runner ~timeout ~steplimit:None prover task
+let compile ~script ~timeout ~memlimit ~config pconf driver prover task =
+ run_batch ~config pconf driver ~script ~timeout ~memlimit ~steplimit:None
+ ~probes:Probe.Map.empty prover task
let prepare ~mode wpo driver task =
let ext = Filename.extension (Why3.Driver.file_of_task driver "S" "T" task) in
@@ -1345,7 +1461,7 @@ let prepare ~mode wpo driver task =
end
else None
-let interactive ~mode wpo pconf ~config driver prover task =
+let interactive ~mode ~config wpo pconf driver prover task =
let time = Wp_parameters.InteractiveTimeout.get () in
let mem = Wp_parameters.Memlimit.get () in
let timeout = if time <= 0 then None else Some (float time) in
@@ -1363,30 +1479,42 @@ let interactive ~mode wpo pconf ~config driver prover task =
Why3.Whyconf.print_prover prover (script :> string) ;
match mode with
| VCS.Batch ->
- compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task
+ compile ~script ~timeout ~memlimit ~config pconf driver prover task
| VCS.Update ->
if merge then updatescript ~script driver task ;
- compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task
+ compile ~script ~timeout ~memlimit ~config pconf driver prover task
| VCS.Edit ->
let open Task in
editor ~script ~merge ~config pconf driver task >>= fun _ ->
- compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task
+ compile ~script ~timeout ~memlimit ~config pconf driver prover task
| VCS.Fix ->
let open Task in
- compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task
+ compile ~script ~timeout ~memlimit ~config pconf driver prover task
>>= fun r ->
if VCS.is_valid r then return r else
editor ~script ~merge ~config pconf driver task >>= fun _ ->
- compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task
+ compile ~script ~timeout ~memlimit ~config pconf driver prover task
| VCS.FixUpdate ->
let open Task in
if merge then updatescript ~script driver task ;
- compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task
+ compile ~script ~timeout ~memlimit ~config pconf driver prover task
>>= fun r ->
if VCS.is_valid r then return r else
let merge = false in
editor ~script ~merge ~config pconf driver task >>= fun _ ->
- compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task
+ compile ~script ~timeout ~memlimit ~config pconf driver prover task
+
+let automated ~config ~probes ~timeout ~steplimit ~memlimit
+ wpo pconf drv prover task =
+ if Wp_parameters.has_out () then output_task wpo drv prover task;
+ if Probe.Map.is_empty probes then
+ Cache.get_result
+ ~digest:(digest_task wpo drv)
+ ~runner:(run_batch ~config ~probes ~memlimit pconf drv ?script:None)
+ ~timeout ~steplimit prover task
+ else
+ run_batch ~config ~probes ~memlimit ~timeout ~steplimit
+ pconf drv prover task
(* -------------------------------------------------------------------------- *)
(* --- Prove WPO --- *)
@@ -1418,7 +1546,13 @@ let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ?memlimit
try
(* Always generate common task *)
let context = Wpo.get_context wpo in
- let task = WpContext.on_context context task_of_wpo wpo in
+ let ce,prover =
+ if Wp_parameters.CounterExamples.get () then
+ match Why3Provers.with_counter_examples prover with
+ | Some prover_ce -> true,prover_ce
+ | None -> false,prover
+ else false, prover in
+ let task,probes = WpContext.on_context context (task_of_wpo ~ce) wpo in
if Wp_parameters.Generate.get ()
then Task.return VCS.no_result (* Only generate *)
else
@@ -1430,12 +1564,10 @@ let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ?memlimit
Task.return VCS.valid
else
if pconf.interactive then
- interactive ~mode wpo pconf ~config drv prover task
+ interactive ~mode ~config wpo pconf drv prover task
else
- Cache.get_result
- ~digest:(digest_task wpo drv)
- ~runner:(run_batch ~config pconf ~memlimit drv ?script:None)
- ~timeout ~steplimit prover task
+ automated ~config ~probes ~timeout ~steplimit ~memlimit
+ wpo pconf drv prover task
with exn ->
if Wp_parameters.has_dkey dkey_api then
Wp_parameters.fatal "[Why3 Error] %a@\n%s"
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index 751717b63be655b0ebcc1e301e51980f0fbf5b71..0dc5e536e08304e28ac273bf06816993ad4cac4c 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -45,7 +45,7 @@ type stats = {
noresult : int ;
failed : int ;
cached : int ;
- cachemiss : int ;
+ cacheable : int ;
}
(* -------------------------------------------------------------------------- *)
@@ -110,12 +110,15 @@ let empty = {
noresult = 0 ;
failed = 0 ;
cached = 0 ;
- cachemiss = 0 ;
+ cacheable = 0 ;
}
-let cacheable p r = p <> Qed && not @@ VCS.is_trivial r
+let cacheable p r =
+ p <> Qed && not @@ VCS.is_trivial r &&
+ VCS.is_auto p && not @@ VCS.has_counter_examples p
+
+let add_cacheable n (p,r) = if cacheable p r then succ n else n
let add_cached n (p,r) = if cacheable p r && r.cached then succ n else n
-let add_cachemiss n (p,r) = if cacheable p r && not r.cached then succ n else n
let results ~smoke results =
let (p,r) = VCS.best results in
@@ -131,7 +134,7 @@ let results ~smoke results =
best = r.verdict ; tactics = 0 ;
proved ; timeout ; unknown ; failed ; noresult ;
cached = List.fold_left add_cached 0 results ;
- cachemiss = List.fold_left add_cachemiss 0 results ;
+ cacheable = List.fold_left add_cacheable 0 results ;
provers =
if p = Qed then [Qed,if smoke then qsmoked r else pqed r]
else
@@ -151,7 +154,7 @@ let add a b =
noresult = a.noresult + b.noresult ;
failed = a.failed + b.failed ;
cached = a.cached + b.cached ;
- cachemiss = a.cachemiss + b.cachemiss ;
+ cacheable = a.cacheable + b.cacheable ;
}
let tactical ~qed children =
@@ -162,7 +165,7 @@ let tactical ~qed children =
List.fold_left add { empty with best ; provers ; tactics = 1 } children
let script stats =
- let cached = stats.cachemiss = 0 in
+ let cached = stats.cached = stats.cacheable in
let solver = List.fold_left
(fun t (p,s) -> if p = Qed then t +. s.time else t) 0.0 stats.provers in
let time = List.fold_left
@@ -207,13 +210,14 @@ let pp_stats ~shell ~cache fmt s =
let updating = Cache.is_updating cache in
let qed_only = match s.provers with [Qed,_] -> true | _ -> false in
let print_cache = not qed_only && Cache.is_active cache in
+ let cachemiss = s.cacheable - s.cached in
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
let print_proofs = success > 0 && total > 1 in
let print_perfo =
pr.time > Rformat.epsilon &&
- (not shell || (not updating && s.cachemiss > 0))
+ (not shell || (not updating && cachemiss > 0))
in
if p != Qed || qed_only || print_perfo || print_proofs
then
@@ -227,21 +231,20 @@ let pp_stats ~shell ~cache fmt s =
Format.fprintf fmt ")"
end
) s.provers ;
- if shell && s.cachemiss > 0 && not updating then
- Format.fprintf fmt " (Cache miss %d)" s.cachemiss
+ if shell && cachemiss > 0 && not updating then
+ Format.fprintf fmt " (Cache miss %d)" cachemiss
else
if print_cache then
- let cacheable = s.cachemiss + s.cached in
- if cacheable = 0 then
+ if s.cacheable = 0 then
if s.best = Valid then
Format.pp_print_string fmt " (Trivial)"
else
Format.pp_print_string fmt " (No Cache)"
else
- if updating || s.cachemiss = 0 then
+ if updating || cachemiss = 0 then
Format.pp_print_string fmt " (Cached)"
else
- Format.fprintf fmt " (Cached %d/%d)" s.cached cacheable
+ Format.fprintf fmt " (Cached %d/%d)" s.cached s.cacheable
let pretty = pp_stats ~shell:false ~cache:NoCache
diff --git a/src/plugins/wp/Stats.mli b/src/plugins/wp/Stats.mli
index 5ac456b19aec6300fdf00a9481bf986c2b5ca95a..ea1cd5dc478d992cba41d0702ae7bc1a41a7a63a 100644
--- a/src/plugins/wp/Stats.mli
+++ b/src/plugins/wp/Stats.mli
@@ -47,7 +47,7 @@ type stats = {
noresult : int ; (** number of no-result sub-goals *)
failed : int ; (** number of failed sub-goals *)
cached : int ; (** number of cached prover results *)
- cachemiss : int ; (** number of non-cached prover results *)
+ cacheable : int ; (** number of prover results that can be cached *)
}
val pp_pstats : Format.formatter -> pstats -> unit
diff --git a/src/plugins/wp/Strategy.ml b/src/plugins/wp/Strategy.ml
index ce46be2cb48423c1cadd404da761628d9d1f2291..acdfb3c00a77dc3c03d637d06accf4fc7b6405d4 100644
--- a/src/plugins/wp/Strategy.ml
+++ b/src/plugins/wp/Strategy.ml
@@ -55,6 +55,8 @@ let occurs_q p q = occurs_e (F.e_prop p) (F.e_prop q)
let lookup_step env queue s =
match s.condition with
| State _ -> Empty
+ | Probe(_,t) ->
+ if t == env.target then Inside(Step s,env.target) else Empty
| When p | Have p | Init p | Core p | Type p ->
let p = Lang.F.e_prop p in
if p == env.target then Clause(Step s) else
diff --git a/src/plugins/wp/TacChoice.ml b/src/plugins/wp/TacChoice.ml
index 27d558c7afbb2b0b75a12c6deec0a8b06c26c022..b760331b12d9dcbbeb1e4b55d517e9c06c744897 100644
--- a/src/plugins/wp/TacChoice.ml
+++ b/src/plugins/wp/TacChoice.ml
@@ -78,7 +78,7 @@ class absurd =
let seq = Conditions.replace ~at:s.id emp seq in
[ "Absurd" , (fst seq , F.p_not p) ]
in Applicable absurd
- | Branch _ | Either _ | State _ ->
+ | Branch _ | Either _ | State _ | Probe _ ->
Not_applicable
end
end
@@ -106,7 +106,7 @@ class contrapose =
let hs = Conditions.replace ~at:s.id goal (hs , F.p_false) in
[ "Contrapose" , (fst hs , F.p_not p) ]
in Applicable contrapose
- | Branch _ | Either _ | State _ ->
+ | Branch _ | Either _ | State _ | Probe _ ->
Not_applicable
end
diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
index 41d5f7d56ec20026d6c59dadf2e775ced00cc3dd..1403da9adbac755c49caa03aabbbbf8f6dd87e0a 100644
--- a/src/plugins/wp/TacInduction.ml
+++ b/src/plugins/wp/TacInduction.ml
@@ -33,6 +33,7 @@ let filter_step n hs s =
match s.Conditions.condition with
| (Have _ | Type _ | Core _ | Init _ | When _) ->
Conditions.map_step (filter_pred n hs) s
+ | Probe _ -> s
| (State _ | Branch _ | Either _) as c ->
if F.Vars.mem n s.vars then
(hs := Conditions.pred_cond c :: !hs ; Conditions.step (Have F.p_true))
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index edbaea2f364b4c23fc2de92e76ad8103c52ffb5e..a73274c60faa70efd4decfa5192bb901bd958797 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -126,8 +126,7 @@ let bind ~side bindings property : Tactical.process =
match side with
| None ->
instance_goal ~title:"Witness" bindings property
- | Some s ->
- let open Conditions in
+ | Some (s : Conditions.step) ->
instance_have ?title:s.descr ~at:s.id bindings property
let filter tau e =
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 6c13ec59f5f7b137615277817ae71043c8dc8a2b..0e1e31f1e1e64650d38e9585f6be8390aa834e96 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -301,7 +301,7 @@ class split =
| Clause(Step step) ->
begin
match step.condition with
- | State _ -> Not_applicable
+ | State _ | Probe _ -> Not_applicable
| Branch(p,_,_) ->
feedback#set_title "Split (branch)" ;
feedback#set_descr "Decompose Conditional into Branches" ;
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 857ba148917782a60ae40d9de246383c23a6e411..1fef10ad99975088ac10a8bc0a17ff13f3108b1b 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -131,6 +131,10 @@ let is_auto = function
not prover_config.interactive
with Not_found -> true
+let has_counter_examples = function
+ | Qed | Tactical -> false
+ | Why3 p -> Why3Provers.with_counter_examples p <> None
+
let cmp_prover p q =
match p,q with
| Qed , Qed -> 0
@@ -209,8 +213,11 @@ type verdict =
| Stepout
| Computing of (unit -> unit) (* kill function *)
| Valid
+ | Invalid (* model *)
| Failed
+type model = Why3Provers.model Probe.Map.t
+
type result = {
verdict : verdict ;
cached : bool ;
@@ -219,10 +226,11 @@ type result = {
prover_steps : int ;
prover_errpos : Lexing.position option ;
prover_errmsg : string ;
+ prover_model : model ;
}
let is_result = function
- | Valid | Unknown | Timeout | Stepout | Failed -> true
+ | Valid | Invalid | Unknown | Timeout | Stepout | Failed -> true
| NoResult | Computing _ -> false
let is_verdict r = is_result r.verdict
@@ -233,7 +241,7 @@ let is_computing = function { verdict=Computing _ } -> true | _ -> false
let is_proved ~smoke = function
| NoResult | Computing _ | Failed -> false
| Valid -> not smoke
- | Unknown | Timeout | Stepout -> smoke
+ | Unknown | Timeout | Stepout | Invalid -> smoke
let configure r =
let valid = (r.verdict = Valid) in
@@ -277,7 +285,7 @@ let autofit r =
time_fits r.prover_time &&
step_fits r.prover_steps
-let result ?(cached=false) ?(solver=0.0) ?(time=0.0) ?(steps=0) verdict =
+let result ?(model=Probe.Map.empty) ?(cached=false) ?(solver=0.0) ?(time=0.0) ?(steps=0) verdict =
{
verdict ;
cached = cached ;
@@ -286,6 +294,7 @@ let result ?(cached=false) ?(solver=0.0) ?(time=0.0) ?(steps=0) verdict =
prover_steps = steps ;
prover_errpos = None ;
prover_errmsg = "" ;
+ prover_model = model;
}
let no_result = result NoResult
@@ -302,6 +311,7 @@ let failed ?pos msg = {
prover_steps = 0 ;
prover_errpos = pos ;
prover_errmsg = msg ;
+ prover_model = Probe.Map.empty ;
}
let cached r = if is_verdict r then { r with cached=true } else r
@@ -330,18 +340,24 @@ let pp_perf_shell fmt r =
let name_of_verdict = function
| NoResult | Computing _ -> "none"
| Valid -> "valid"
+ | Invalid -> "invalid"
| Failed -> "failed"
| Unknown -> "unknown"
| Stepout -> "stepout"
| Timeout -> "timeout"
+let pp_hasmodel fmt (r : result) =
+ if not @@ Probe.Map.is_empty r.prover_model then
+ Format.fprintf fmt " (Model)"
+
let pp_result fmt r =
match r.verdict with
| NoResult -> Format.pp_print_string fmt "No Result"
| Computing _ -> Format.pp_print_string fmt "Computing"
| Failed -> Format.fprintf fmt "Failed@ %s" r.prover_errmsg
| Valid -> Format.fprintf fmt "Valid%a" pp_perf_shell r
- | Unknown -> Format.fprintf fmt "Unknown%a" pp_perf_shell r
+ | Invalid -> Format.fprintf fmt "Invalid%a" pp_hasmodel r
+ | Unknown -> Format.fprintf fmt "Unknown%a%a" pp_hasmodel r pp_perf_shell r
| Stepout -> Format.fprintf fmt "Step limit%a" pp_perf_shell r
| Timeout -> Format.fprintf fmt "Timeout%a" pp_perf_shell r
@@ -357,8 +373,10 @@ let pp_cache_miss fmt st updating prover result =
then
Format.fprintf fmt "%s%a (missing cache)" st pp_perf_forced result
else
- Format.pp_print_string fmt @@
- if is_valid result then "Valid" else "Unsuccess"
+ if is_valid result then
+ Format.pp_print_string fmt "Valid"
+ else
+ Format.fprintf fmt "Unsuccess%a" pp_hasmodel result
let pp_result_qualif ?(updating=true) prover result fmt =
if Wp_parameters.has_dkey dkey_shell then
@@ -367,13 +385,20 @@ let pp_result_qualif ?(updating=true) prover result fmt =
| Computing _ -> Format.pp_print_string fmt "Computing"
| Failed -> Format.fprintf fmt "Failed@ %s" result.prover_errmsg
| Valid -> pp_cache_miss fmt "Valid" updating prover result
+ | Invalid -> pp_cache_miss fmt "Invalid" updating prover result
| Unknown -> pp_cache_miss fmt "Unsuccess" updating prover result
| Timeout -> pp_cache_miss fmt "Timeout" updating prover result
| Stepout -> pp_cache_miss fmt "Stepout" updating prover result
else
pp_result fmt result
-(* highest is best *)
+let pp_model fmt model =
+ Probe.Map.iter
+ (fun probe model ->
+ Format.fprintf fmt "@[<hov 2>Model %a = %a@]@\n"
+ Probe.pretty probe Why3Provers.pp_model model
+ ) model
+
let vrank = function
| Computing _ -> 0
| NoResult -> 1
@@ -382,6 +407,7 @@ let vrank = function
| Timeout -> 4
| Stepout -> 5
| Valid -> 6
+ | Invalid -> 7
let conjunction a b =
match a,b with
@@ -390,14 +416,22 @@ let conjunction a b =
| r , Valid -> r
| _ -> if vrank b > vrank a then b else a
+let msize m = Probe.Map.fold (fun _ _ n -> succ n) m 0
+
let compare p q =
- let r = vrank q.verdict - vrank p.verdict in
- if r <> 0 then r else
- let s = Stdlib.compare p.prover_steps q.prover_steps in
+ match is_valid p , is_valid q with
+ | true , false -> (-1)
+ | false , true -> (+1)
+ | _ ->
+ let s = msize q.prover_model - msize p.prover_model in
if s <> 0 then s else
- let t = Stdlib.compare p.prover_time q.prover_time in
- if t <> 0 then t else
- Stdlib.compare p.solver_time q.solver_time
+ let r = vrank q.verdict - vrank p.verdict in
+ if r <> 0 then r else
+ let s = Stdlib.compare p.prover_steps q.prover_steps in
+ if s <> 0 then s else
+ let t = Stdlib.compare p.prover_time q.prover_time in
+ if t <> 0 then t else
+ Stdlib.compare p.solver_time q.solver_time
let bestp pr1 pr2 = if compare (snd pr1) (snd pr2) <= 0 then pr1 else pr2
let best = List.fold_left bestp (Qed,no_result)
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 4cdd7100839840271af0468fe3315d004a44a0aa..62a7f6b5d91a1546eccaaaba409ee49884e0f22e 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -92,8 +92,11 @@ type verdict =
| Stepout
| Computing of (unit -> unit) (* kill function *)
| Valid
+ | Invalid (* model *)
| Failed
+type model = Why3Provers.model Probe.Map.t
+
type result = {
verdict : verdict ;
cached : bool ;
@@ -102,6 +105,7 @@ type result = {
prover_steps : int ;
prover_errpos : Lexing.position option ;
prover_errmsg : string ;
+ prover_model : model ;
}
val no_result : result
@@ -114,9 +118,11 @@ val failed : ?pos:Lexing.position -> string -> result
val kfailed : ?pos:Lexing.position -> ('a,Format.formatter,unit,result) format4 -> 'a
val cached : result -> result (** only for true verdicts *)
-val result : ?cached:bool -> ?solver:float -> ?time:float -> ?steps:int -> verdict -> result
+val result : ?model:model -> ?cached:bool ->
+ ?solver:float -> ?time:float -> ?steps:int -> verdict -> result
val is_auto : prover -> bool
+val has_counter_examples : prover -> bool
val is_prover : prover -> bool
val is_result : verdict -> bool
val is_verdict : result -> bool
@@ -132,6 +138,7 @@ val autofit : result -> bool (** Result that fits the default configuration *)
val name_of_verdict : verdict -> string
val pp_result : Format.formatter -> result -> unit
+val pp_model : Format.formatter -> model -> unit
val pp_result_qualif : ?updating:bool -> prover -> result ->
Format.formatter -> unit
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 38a9e97129761c0fae3e4dae9a1904f9c1e6b3be..2a958392965192ef88c06af011782957f59be145 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -103,6 +103,9 @@ let title ?(version=true) p =
else p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
let is_mainstream p = p.Why3.Whyconf.prover_altern = ""
+let has_counter_examples p =
+ List.mem "counterexamples" @@
+ String.split_on_char '+' p.Why3.Whyconf.prover_altern
let provers () =
Why3.Whyconf.Mprover.keys (Why3.Whyconf.get_provers (config ()))
@@ -119,4 +122,18 @@ let has_shortcut p s =
| None -> false
| Some p' -> Why3.Whyconf.Prover.equal p p'
+let with_counter_examples p =
+ if has_counter_examples p then Some p else
+ let name = p.prover_name in
+ List.find_opt
+ (fun (q : t) -> q.prover_name = name && has_counter_examples q)
+ @@ provers ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Models --- *)
+(* -------------------------------------------------------------------------- *)
+
+type model = Why3.Model_parser.concrete_syntax_term
+let pp_model = Why3.Model_parser.print_concrete_term
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 1db0e9baca5fff878fabe171193c101217736217..7992e2b140e31a5bcb2875896f5be6fca71d9924 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -41,6 +41,12 @@ val provers : unit -> t list
val provers_set : unit -> Why3.Whyconf.Sprover.t
val is_available : t -> bool
val is_mainstream : t -> bool
+val has_counter_examples : t -> bool
+val with_counter_examples : t -> t option
val has_shortcut : t -> string -> bool
+
+type model = Why3.Model_parser.concrete_syntax_term
+val pp_model : model Pretty_utils.formatter
+
(**************************************************************************)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 38bbdb98b0a8099861d3ae4cba5f747d5e0b67b7..ab494fb2497ada67372a7d7cccfd7ae5bfd734f5 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -226,8 +226,12 @@ struct
opt_fold (prove_property env) code_verified @@
opt_fold (use_property env) code_admitted w
in
+ let probes = Probe.annotations s in
+ let do_probe env (probe,term) =
+ W.add_probe env.we ~stmt:s probe term in
let pi =
W.label env.we (Some s) (Clabels.stmt s) @@
+ List.fold_right (do_probe env) probes @@
List.fold_right (do_assert env) cas @@
control env a s
in
@@ -466,6 +470,13 @@ struct
I.process_global_init env.we env.mode.kf @@
W.scope env.we [] SC_Global w
+ let do_probe_formal env x w =
+ let probes = Wp_parameters.CounterExamples.get () in
+ if probes then
+ let term = Cil_builder.Exp.(cil_term ~loc:x.vdecl @@ var x) in
+ W.add_probe env.we x.vname term w
+ else w
+
let do_preconditions env ~formals (b : CfgAnnot.behavior) w =
let kf = env.mode.kf in
let init = CfgInfos.is_entry_point kf in
@@ -482,6 +493,7 @@ struct
List.fold_right (use_property env) b.bhv_requires @@
List.fold_right (prove_property env) b.bhv_smokes @@
List.fold_right (use_property env) side_behaviors @@
+ List.fold_right (do_probe_formal env) formals @@
(* frame-in *)
W.scope env.we formals SC_Frame_in w
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index f62ff22ea6d025ac733334260a9ba83bde191888..d33831400fab4b910dc8a954fb52ac8735e571d6 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -89,6 +89,16 @@ let new_env ?lvars kf : t_env = ignore lvars ; kf
let add_axiom _p _l = ()
+let add_probe _env ?stmt p t k =
+ ignore stmt ;
+ let u = node () in
+ if Wp_parameters.debug_atleast 1 then
+ Format.fprintf !out " %a [ label=\"Probe %a\" ] ;@." pretty u Printer.pp_term t
+ else
+ Format.fprintf !out " %a [ label=\"Probe %s\" ] ;@." pretty u p ;
+ Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+ link u k ; u
+
let add_hyp ?for_pid _env (pid,pred) k =
ignore(for_pid);
let u = node () in
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index c43def5003d3af4a6f85c1bbf2e1ddd8fc5455a6..337e1a2fb00afffcc41a8e133c1da20c85d7c7e6 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -303,6 +303,19 @@ struct
path = path ;
}
+ let probe_vc ~loc ?descr ?stmt ?warn ~name term vc =
+ let vars = F.vars term in
+ let hyps = Conditions.probe ~loc ?descr ?stmt ~name term vc.hyps in
+ let wrns = match warn with
+ | None -> vc.warn
+ | Some w -> Warning.Set.union w vc.warn in
+ { hyps = hyps ;
+ vars = vars ;
+ warn = wrns ;
+ goal = vc.goal ;
+ deps = vc.deps ;
+ path = vc.path }
+
(* -------------------------------------------------------------------------- *)
(* --- Branching --- *)
(* -------------------------------------------------------------------------- *)
@@ -366,12 +379,7 @@ struct
let deps = List.fold_left (fun d vc -> D.union d vc.deps) D.empty vcs in
let warn = List.fold_left (fun d vc -> W.union d vc.warn) W.empty vcs in
let path = List.fold_left (fun d vc -> S.union d vc.path) S.empty vcs in
- { hyps = hyps ;
- goal = goal ;
- vars = vars ;
- deps = deps ;
- warn = warn ;
- path = path }
+ { hyps ; goal ; vars ; deps ; warn ; path }
(* -------------------------------------------------------------------------- *)
(* --- Merging and Branching with Splitters --- *)
@@ -527,6 +535,19 @@ struct
let add_axiom _id _l = ()
+ let add_probe wenv ?stmt probe term wp = in_wenv wenv wp
+ (fun env wp ->
+ let outcome =
+ Warning.catch
+ ~severe:false ~effect:"Skip probe"
+ (L.term env) term in
+ match outcome with
+ | Warning.Failed _warn -> wp
+ | Warning.Result(warn,value) ->
+ let add_probe_vc =
+ probe_vc ~loc:term.term_loc ?stmt ~warn ~name:probe value in
+ { wp with vcs = gmap add_probe_vc wp.vcs })
+
let add_hyp ?for_pid wenv (hpid,predicate) wp = in_wenv wenv wp
(fun env wp ->
let outcome = Warning.catch
@@ -1439,9 +1460,9 @@ struct
(* -------------------------------------------------------------------------- *)
let wp_scope env wp ~descr scope xs =
- let post = L.current env in
- let pre = M.alloc post xs in
- let hs = M.scope { pre ; post } scope xs in
+ let sigma = L.current env in
+ let pre = M.alloc sigma xs in
+ let hs = M.scope { pre ; post = sigma } scope xs in
let vcs = gmap (assume_vc ~descr hs) wp.vcs in
{ wp with sigma = Some pre ; vcs = vcs }
@@ -1631,7 +1652,7 @@ struct
let id = WpPropId.mk_lemma_id l in
let def = L.lemma l in
let model = WpContext.get_model () in
- let sequent = Conditions.lemma def.l_lemma in
+ let sequent = Conditions.lemma ~loc:l.lem_loc def.l_lemma in
let vca = {
Wpo.VC_Annot.axioms = Some (def.l_cluster, l.lem_depends) ;
goal = GOAL.make sequent ;
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 1fe93a479d2e507698e3169d3b90919429915f43..8c6f6ae198dd42769f4294a21206d70ea4c03b79 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1227,7 +1227,7 @@ would never be provable.
The \textsf{WP} plug-in can generate smoke-tests to detect such inconsistencies.
Basically, it consists in checking if \verb+\false+ is provable under the requirements
-or assumptions of a behaviour, or under the invariants of a loop. Also, a simple reachability
+or assumptions of a behavior, or under the invariants of a loop. Also, a simple reachability
analysis is performed to track dead-code statements and calls that neither terminates nor exits.
This is best-effort verification : if at least one prover succeed in proving \verb+\false+,
@@ -1494,6 +1494,146 @@ obligations are:
yet. Its content is not cleaned up automatically.
\end{description}
+\subsection{Probes and Counter Examples}
+
+\emph{Introduced since Frama-C 29.0 (Copper)}
+
+Depending on prover capabilities, \textsf{WP} can trigger counter example
+generation for non successful goals. Provers supporting counter example
+generation can be identified by the \verb$"counterexamples"$ variant after their
+name. For example, in the prover selection example above, \verb+cvc4-ce+ and
+\verb+z3-ce+ are such provers.
+
+To enable counter examples generation by \textsf{WP} you shall use
+\verb+-wp-counter-examples+ option. Then, for each selected solver that has a
+counter-examples variant, this variant will be used instead and counter-examples
+will be asked to the solver in case of unknown result. Notice that you can also
+use counter-examples solvers \emph{without} asking for counter-examples. For
+instance, with option \verb+-wp-prover cvc4-ce+, \textsf{WP} will use this
+version of the prover, even if counter examples is not active; the prover will
+not be asked to report models, unless counter examples \emph{is}
+activate. Notice that solvers variants with counter-examples support are
+generally a bit slower than their original version.
+
+A proof obligation for which a counter-example has been generated is reported by
+\textsf{WP} by the string \verb+"(Model)"+ after its proof status. For instance:
+
+\begin{shell}
+# ./bin/frama-c -wp ~/work/wrong.i -wp-prover cvc4 -wp-counter-examples
+[...]
+[wp] 6 goals scheduled
+[wp] [Unknown] typed_g_ensures (Qed 4ms) (CVC4) (No Cache) (Model)
+[wp] [Cache] not used
+[wp] Proved goals: 6 / 7
+ Unreachable: 1
+ Qed: 5 (0.72ms)
+ Unknown: 1
+\end{shell}
+
+Notice that cache usage is disabled for provers asked to generate a
+counter-example, since models are currently not stored in \textsf{WP}'s
+cache\footnote{This feature might be added in future versions of the plugin.}.
+
+A counter-example consists in a \emph{Model}, that is, a map from
+\emph{Variables} or \emph{Probes} (see below) to \emph{Values}, for which the
+proof obligation formula is expected to be \verb+False+. More precisely, the
+Model reports on \emph{necessary} conditions for the proof obligation to be
+wrong, although they might not be \emph{sufficient} in practice.
+
+Generated models are reported by \textsf{WP} along with prover results when
+either \verb+-wp-print+ or \verb+-wp-status+ options are used. The interactive
+proof transformer (\textsf{TIP}) also displays models in the graphical user
+interface, when available.
+
+Probes are generalization of variables. They are named expressions for which the
+prover is asked to output a value in the model. \textsf{WP} will automatically
+introduce probes for formal parameters of functions and universally quantified
+variables of lemmas. Developers can introduce their own probes by using the
+\verb+@probe+ annotation. For instance:
+
+\begin{lstlisting}[style=c]
+ int a[4][5];
+ /*@
+ ensures \false;
+ assigns \nothing;
+ */
+ int value(int i, int j) {
+ //@ probe Offset: &a[i][j] - &a[0][0];
+ return a[i][j];
+ }
+}
+\end{lstlisting}
+
+Probes \emph{must} be named \textsf{ACSL} terms. As a short cut, for very
+simple probes such as variables, the name can be omitted. Several probes might
+have the same name, although it is not really convenient for debugging. The
+general syntax for the annotation is:
+\[
+\mathtt{probe} \; a_1: t_1, \ldots, a_n: t_n \;\mathtt{;}
+\]
+
+Probes are normalized by \textsf{Qed} during simplification of proof obligations
+by \textsf{WP}. Their (simplified) term definitions are reported when printing
+proof obligations, and their model values are reported when printing proof
+results, when available. For instance:
+
+\begin{shell}
+ # frama-c [...] -wp-status
+ [...]
+ Goal Post-condition (file /Users/correnson/work/matrix.i, line 3) in 'value':
+ Assume {
+ Type: is_sint32(i) /\ is_sint32(j).
+ Probe i = i.
+ Probe j = j.
+ Probe Offset = ((4 * j) + (20 * i)) / 4.
+ }
+ Prove: false.
+ Prover CVC4 1.8 returns Unknown (Model) (Qed:2ms)
+ Model i = 0
+ Model j = 0
+ Model Offset = 0
+ [...]
+\end{shell}
+
+User probes are always reported, even if \verb+-wp-counter-examples+ is not
+activated. This feature reveals to be extremely useful for debugging proofs in
+practice, even when counter examples is not available or not activated. It also
+helps in understanding \textsf{C}, \textsf{ACSL} and \textsf{WP} models and
+encoding.
+
+You may freely add as many probes as you want: probes do not modify the
+proof obligations submitted to the provers, unless \verb+-wp-counter-examples+
+is activated. For instance, in the previous example:
+
+\begin{shell}
+ # frama-c [...] -wp-status -wp-no-counter-examples
+ [...]
+ Goal Post-condition (file /Users/correnson/work/matrix.i, line 3) in 'value':
+ Assume {
+ Type: is_sint32(i) /\ is_sint32(j).
+ Probe Offset = ((4 * j) + (20 * i)) / 4.
+ }
+ Prove: false.
+ Prover CVC4 1.8 returns Unknown (Qed:2ms) (Cached)
+ [...]
+\end{shell}
+
+\noindent
+Summary of \textsf{WP} options related to probes and counter-examples generation:
+\begin{description}
+\item[\tt -wp-(no)-counter-examples] enables counter examples generation for
+ supporting provers. Also generate probes for formal parameters of functions
+ and universal quantifiers of lemmas. Not set by default.
+\item[\tt -wp-print, -wp-status] pretty-prints the probes and the associated models,
+ when available.
+\item[\tt -wp-solver xxx-ce] use the specified variant of prover, even
+ when counter-examples is not activated.
+\item[\tt -wp-(no)-probes] registers the \verb+@probe+ \textsf{ACSL}
+ extension in \textsf{Frama-C} kernel.
+ This option is set by default, but you may want to deactivate it to
+ avoid any clash with extensions from other plugins.
+\end{description}
+
\subsection{Additional Proof Libraries}
\label{prooflibs}
diff --git a/src/plugins/wp/gui/GuiList.ml b/src/plugins/wp/gui/GuiList.ml
index 149c4edbef0dc558565a89822d19d9d30741ea77..4d694a5326392e5fe2dd00b9ef54aafaebbe81ad 100644
--- a/src/plugins/wp/gui/GuiList.ml
+++ b/src/plugins/wp/gui/GuiList.ml
@@ -54,6 +54,7 @@ let render_prover_result p =
let icon_of_verdict ~smoke = function
| NoResult -> icn_none
| Valid -> if smoke then icn_invalid else icn_valid
+ | Invalid -> if smoke then icn_valid else icn_invalid
| Unknown -> if smoke then icn_valid else icn_unknown
| Timeout | Stepout -> if smoke then icn_valid else icn_cut
| Failed -> icn_failed
diff --git a/src/plugins/wp/gui/GuiProof.ml b/src/plugins/wp/gui/GuiProof.ml
index df6db9048c1dc7a2a9789be508ae8a159f649d31..390f2a7e2759f93d4e69ca0affb209e7d954e2fd 100644
--- a/src/plugins/wp/gui/GuiProof.ml
+++ b/src/plugins/wp/gui/GuiProof.ml
@@ -60,7 +60,7 @@ class printer (text : Wtext.text) =
text#printf "@{<bf>Prover@} %a: @{<green>%a@}.@\n"
VCS.pp_prover prv VCS.pp_result res
else
- text#printf "@{<bf>Prover@} %a: @{<green>%a@}.@\n"
+ text#printf "@{<bf>Prover@} %a: @{<orange>%a@}.@\n"
VCS.pp_prover prv VCS.pp_result res
) (Wpo.get_results wpo)
diff --git a/src/plugins/wp/gui/GuiProver.ml b/src/plugins/wp/gui/GuiProver.ml
index 64c87a6af4697dc4610f133e103f0116eb1b6600..792592208198d06176cf9f9384d32aec36bfc960 100644
--- a/src/plugins/wp/gui/GuiProver.ml
+++ b/src/plugins/wp/gui/GuiProver.ml
@@ -78,7 +78,9 @@ class prover ~(console:Wtext.text) ~prover =
let lerr = Filepath.exists ferr in
if lout || lerr then console#hrule ;
console#scroll () ;
- console#printf "[%a] %a@." VCS.pp_prover prover VCS.pp_result res ;
+ console#printf "[%a] %a@.%a" VCS.pp_prover prover
+ VCS.pp_result res
+ VCS.pp_model res.prover_model ;
if lout then Command.pp_from_file console#fmt fout ;
if lerr then Command.pp_from_file console#fmt ferr ;
if lout || lerr then console#hrule ;
@@ -134,7 +136,7 @@ class prover ~(console:Wtext.text) ~prover =
self#set_action ~tooltip:"Run Prover" ~icon:`MEDIA_PLAY ~callback () ;
Pretty_utils.ksfprintf self#set_label "%a (%a)" VCS.pp_prover prover
Rformat.pp_time res.VCS.prover_time ;
- | VCS.Unknown | VCS.Timeout | VCS.Stepout ->
+ | VCS.Unknown | VCS.Timeout | VCS.Stepout | VCS.Invalid ->
let callback () = self#run wpo in
self#set_status ko_status ;
self#set_action ~tooltip:"Run Prover" ~icon:`MEDIA_PLAY ~callback () ;
diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.ml
index 4a7d416a81469a627be953e577d2ffdfc00f8074..d746f4ba4aace5dc43ef1c9d87c8c318aa08e200 100644
--- a/src/plugins/wp/mcfg.ml
+++ b/src/plugins/wp/mcfg.ml
@@ -82,6 +82,9 @@ module type S = sig
val new_env : ?lvars:Cil_types.logic_var list -> kernel_function -> t_env
val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit
+
+ val add_probe : t_env -> ?stmt:stmt -> string -> term -> t_prop -> t_prop
+
val add_hyp :
?for_pid:WpPropId.prop_id -> t_env -> WpPropId.pred_info -> t_prop -> t_prop
val add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop
diff --git a/src/plugins/wp/ptip.ml b/src/plugins/wp/ptip.ml
index 8254af45dec226d150a2aff778224021c2318ca1..76c0393e81500d32f4836c81862b01646a846117 100644
--- a/src/plugins/wp/ptip.ml
+++ b/src/plugins/wp/ptip.ml
@@ -151,6 +151,7 @@ class autofocus =
match step.condition with
| When _ -> true
| State s -> self#occurs_state s
+ | Probe(_,t) -> self#occurs_term t
| Init p | Have p | Type p | Core p ->
self#occurs_term (F.e_prop p)
| Branch(p,sa,sb) ->
@@ -246,12 +247,13 @@ class autofocus =
then Tactical.(Inside(Goal goal,a))
else
let pool = ref Tactical.Empty in
- let lookup_pred s a p =
- if F.is_subterm a (F.e_prop p) then
+ let lookup_term s a t =
+ if F.is_subterm a t then
begin
pool := Tactical.(Inside(Step s,a));
raise Exit;
end in
+ let lookup_pred s a p = lookup_term s a (F.e_prop p) in
let rec lookup_sequence a hs =
(*TODO: staged iter *)
Conditions.iter
@@ -259,6 +261,7 @@ class autofocus =
match step.condition with
| (Type p | Init p | Have p | When p | Core p)
-> lookup_pred step a p
+ | Probe(_,t) -> lookup_term step a t
| Branch(p,sa,sb) ->
lookup_pred step a p ;
lookup_sequence a sa ;
@@ -385,6 +388,8 @@ class pcond
begin
match step.condition with
| State _ -> ()
+ | Probe(_,t) ->
+ domain <- Vars.union (F.vars t) domain
| Have p | Init p | Core p | When p | Type p ->
domain <- Vars.union (F.varsp p) domain
| Branch(p,a,b) ->
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 2805cea703ab916916177edd3b987d6f41ea8f09..eca897451ea5a8d0498ad46dc1526b67ada578f2 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -354,6 +354,20 @@ let do_wpo_result goal prover res =
if VCS.is_verdict res && prover = VCS.Qed then
do_progress goal "Qed"
+let pp_hasmodel fmt goal =
+ if Wp_parameters.CounterExamples.get () then
+ let results = Wpo.get_results goal in
+ let model =
+ List.exists
+ (fun (_,r) -> not @@ Probe.Map.is_empty r.VCS.prover_model)
+ results in
+ if model then Format.fprintf fmt " (Model)" else
+ let ce_variant =
+ List.exists
+ (fun (p,_) -> VCS.has_counter_examples p)
+ results in
+ if ce_variant then Format.fprintf fmt " (No Model)"
+
let do_report_stats ~shell ~cache ~smoke goal (stats : Stats.stats) =
let status =
if smoke then
@@ -361,25 +375,27 @@ let do_report_stats ~shell ~cache ~smoke goal (stats : Stats.stats) =
| Valid -> "[Failed] (Doomed)"
| Failed -> "[Failure] (Solver Error)"
| NoResult | Computing _ -> "[NoResult] (Unknown)"
- | (Unknown | Timeout | Stepout) when shell -> "[Passed] (Unsuccess)"
+ | (Unknown | Timeout | Stepout | Invalid)
+ when shell -> "[Passed] (Unsuccess)"
| Unknown -> "[Passed] (Unknown)"
| Timeout -> "[Passed] (Timeout)"
| Stepout -> "[Passed] (Stepout)"
+ | Invalid -> "[Passed] (Invalid)"
else
match stats.best with
| NoResult when shell -> "[NoResult]"
| NoResult | Computing _ -> ""
| Valid -> "[Valid]"
| Failed -> "[Failure]"
- | (Unknown | Timeout | Stepout) when shell -> "[Unsuccess]"
+ | (Invalid | Unknown | Timeout | Stepout) when shell -> "[Unsuccess]"
| Unknown -> "[Unknown]"
| Timeout -> "[Timeout]"
| Stepout -> "[Stepout]"
- in
- if status <> "" then
- Wp_parameters.feedback "%s %s%a%a"
+ | Invalid -> "[Invalid]"
+ in if status <> "" then
+ Wp_parameters.feedback "%s %s%a%a%a"
status (Wpo.get_gid goal) (Stats.pp_stats ~shell ~cache) stats
- pp_warnings goal
+ pp_hasmodel goal pp_warnings goal
let do_wpo_success ~shell ~cache goal success =
if Wp_parameters.Generate.get () then
diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config
index d53499bf328b942033d55884fabd3a78cb101437..5221e8c0f16237b724d4e1a878776e1b22e8ac88 100644
--- a/src/plugins/wp/tests/ptests_config
+++ b/src/plugins/wp/tests/ptests_config
@@ -1,6 +1,8 @@
-DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
+DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare
DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
qualif_SUITES= why3
+
+ce_SUITES= wp_ce
diff --git a/src/plugins/wp/tests/wp_ce/cvc4_ce.i b/src/plugins/wp/tests/wp_ce/cvc4_ce.i
new file mode 100644
index 0000000000000000000000000000000000000000..cff74da54d769ae6297aaf89277bb77ef8f7a903
--- /dev/null
+++ b/src/plugins/wp/tests/wp_ce/cvc4_ce.i
@@ -0,0 +1,12 @@
+/* run.config_ce
+ OPT: -wp -wp-counter-examples -wp-prover cvc4 -wp-status
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+
+//@ check lemma wrong: \forall integer x; \abs(x) == x;
+
+//@ ensures \result == \abs(x); assigns \nothing;
+int wrong(int x) { return x; }
diff --git a/src/plugins/wp/tests/wp_ce/oracle/cvc4_ce.res.oracle b/src/plugins/wp/tests/wp_ce/oracle/cvc4_ce.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c98d32bed6cbbdca6bf035c488bd49c632813e4f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_ce/oracle/cvc4_ce.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp [...]
+[kernel] Parsing cvc4_ce.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal wrong_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal wrong_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Check Lemma 'wrong':
+Prove: IAbs.abs(x) = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function wrong
+------------------------------------------------------------
+
+Goal Post-condition (file cvc4_ce.i, line 11) in 'wrong':
+Assume { Type: is_sint32(wrong_0). }
+Prove: IAbs.abs(wrong_0) = wrong_0.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'wrong':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_ce/oracle/probes.res.oracle b/src/plugins/wp/tests/wp_ce/oracle/probes.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cc0cb7183aad041b65eb3c24fdea44633f5bc363
--- /dev/null
+++ b/src/plugins/wp/tests/wp_ce/oracle/probes.res.oracle
@@ -0,0 +1,50 @@
+# frama-c -wp [...]
+[kernel] Parsing probes.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal get_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal get_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function get
+------------------------------------------------------------
+
+Goal Post-condition (file probes.i, line 12) in 'get':
+Let x = -i_2.
+Assume {
+ Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
+ is_sint32(i_4) /\ is_sint32(j) /\ is_sint32(k).
+ If i_2 != 0
+ Then { Have: (1 + i_2) = i_3. }
+ Else { Have: i_3 = 0. }
+ If j != 0
+ Then { Have: i_4 = i_3. Have: (1 + i_3) = i_1. }
+ Else { Have: i_3 = i_1. }
+ If k != 0
+ Then { Have: (1 + i_1) = i. }
+ Else { Have: i_1 = i. }
+ Probe A = 0.
+ Probe B = i_3 - i_2.
+ Probe C = i_1 - i_2.
+ Probe Offset = ((4 * k) + (20 * j) + (80 * i)) / 4.
+}
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'get' (1/3):
+Effect at line 16
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'get' (2/3):
+Effect at line 18
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'get' (3/3):
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_ce/oracle_ce/cvc4_ce.res.oracle b/src/plugins/wp/tests/wp_ce/oracle_ce/cvc4_ce.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ab352704f50f31c4760de5dc3ad56b17d932c8d8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_ce/oracle_ce/cvc4_ce.res.oracle
@@ -0,0 +1,44 @@
+# frama-c -wp [...]
+[kernel] Parsing cvc4_ce.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal wrong_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal wrong_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Unsuccess] typed_check_lemma_wrong (CVC4) (Model)
+[wp] [Unsuccess] typed_wrong_ensures (CVC4) (Model)
+[wp] [Valid] typed_wrong_assigns (Qed)
+[wp] Proved goals: 3 / 5
+ Terminating: 1
+ Unreachable: 1
+ Qed: 1
+ Unsuccess: 2
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Check Lemma 'wrong':
+Assume { Probe x = x. }
+Prove: IAbs.abs(x) = x.
+Prover CVC4 returns Unsuccess (Model)
+Model x = -1
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function wrong
+------------------------------------------------------------
+
+Goal Post-condition (file cvc4_ce.i, line 11) in 'wrong':
+Assume { Type: is_sint32(wrong_0). Probe x = wrong_0. }
+Prove: IAbs.abs(wrong_0) = wrong_0.
+Prover CVC4 returns Unsuccess (Model)
+Model x = -1
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - - 1 0.0%
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ wrong 1 - 2 50.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_ce/probes.i b/src/plugins/wp/tests/wp_ce/probes.i
new file mode 100644
index 0000000000000000000000000000000000000000..03ccb78a4337863619222551aeefb45cf07fbdbf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_ce/probes.i
@@ -0,0 +1,26 @@
+/* run.config_qualif
+ DONTRUN:
+*/
+/* run.config_ce
+ DONTRUN:
+*/
+
+// Matrix addessing
+
+int a[3][4][5];
+
+//@ ensures \false; assigns \nothing;
+void get(int i, int j, int k)
+{
+ A:
+ if (i) i++;
+ B:
+ if (j) i++;
+ C:
+ if (k) i++;
+ //@ probe A: \at(i,A) - \at(i,Pre);
+ //@ probe B: \at(i,B) - \at(i,Pre);
+ //@ probe C: \at(i,C) - \at(i,Pre);
+ //@ probe Offset: &a[i][j][k] - &a[0][0][0];
+ return;
+}
diff --git a/src/plugins/wp/tests/wp_ce/test_config_ce b/src/plugins/wp/tests/wp_ce/test_config_ce
new file mode 100644
index 0000000000000000000000000000000000000000..c3e8d3e1aaf369e619027b1cb1ee1b33eb789d0b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_ce/test_config_ce
@@ -0,0 +1,3 @@
+PLUGIN: wp
+CMD: @frama-c@ -wp -wp-par 1 -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report %{dep:@PTEST_SUITE_DIR@/../qualif.report} -wp-cache none
+OPT:
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 26910b42448f6a4b5ed06ceec7f6e9358b5c85b6..fb612438d63376095cbad85324c2ff2f114cdbd3 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -125,6 +125,7 @@ struct
`String begin
match verdict with
| Valid -> if smoke then "DOOMED" else "VALID"
+ | Invalid -> if smoke then "PASSED" else "INVALID"
| Unknown -> if smoke then "PASSED" else "UNKNOWN"
| Timeout -> if smoke then "PASSED" else "TIMEOUT"
| Stepout -> if smoke then "PASSED" else "STEPOUT"
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index 32ab774e70e187994330774435391bb5b18935cf..893a7df45fbc9bdf77c46c67e55a790851614a71 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -97,7 +97,7 @@ let result ~status ~smoke (r:VCS.result) =
match r.VCS.verdict with
| VCS.NoResult | VCS.Computing _ -> NORESULT
| VCS.Failed -> INCONCLUSIVE
- | VCS.Unknown | VCS.Timeout | VCS.Stepout ->
+ | VCS.Unknown | VCS.Timeout | VCS.Stepout | VCS.Invalid ->
if smoke then VALID else UNSUCCESS
| VCS.Valid ->
if smoke then UNSUCCESS else VALID
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index fa160ed4b0afc590811632467727bed6a8503a56..aa558367890b812aec77a6c21dd81f4f8ec083f6 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1152,6 +1152,20 @@ module OutputDir =
Defaults to some temporary directory."
end)
+module Probes =
+ True
+ (struct
+ let option_name = "-wp-probes"
+ let help = "Activate user-defines probes (@probe) (default: yes)"
+ end)
+
+module CounterExamples =
+ False
+ (struct
+ let option_name = "-wp-counter-examples"
+ let help = "Ask for counter examples when supported by provers"
+ end)
+
(* -------------------------------------------------------------------------- *)
(* --- Output Dir --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index ee692cfe9f0d8bdc3b200d23a2c1261db960caca..02ddb77250bba27096a59804668363c1282a48a6 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -164,6 +164,8 @@ module SmokeDeadcode: Parameter_sig.Bool
module SmokeDeadcall: Parameter_sig.Bool
module SmokeDeadlocalinit: Parameter_sig.Bool
module SmokeDeadloop: Parameter_sig.Bool
+module Probes: Parameter_sig.Bool
+module CounterExamples: Parameter_sig.Bool
(** {2 Getters} *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 578e5b974f3d8f39ccf13924c980f9e9e54d1758..94995e8bb72c47a7ee64e08cdbac4866b01a4fce 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -109,7 +109,9 @@ struct
mutable time : float ;
mutable simplified : bool ;
mutable sequent : Conditions.sequent ;
- mutable obligation : F.pred ;
+ mutable opened : F.pred ;
+ mutable closed : F.pred ;
+ mutable probes : F.term Probe.Map.t ;
}
let empty = Conditions.empty
@@ -118,21 +120,27 @@ struct
time = 0.0 ;
simplified = false ;
sequent = empty , F.p_false ;
- obligation = F.p_false ;
+ opened = F.p_false ;
+ closed = F.p_false ;
+ probes = Probe.Map.empty ;
}
let trivial = {
time = 0.0 ;
simplified = true ;
sequent = empty , F.p_true ;
- obligation = F.p_true ;
+ opened = F.p_true ;
+ closed = F.p_true ;
+ probes = Probe.Map.empty ;
}
let make sequent = {
time = 0.0 ;
simplified = false ;
sequent = sequent ;
- obligation = F.p_false ;
+ opened = F.p_false ;
+ closed = F.p_false ;
+ probes = Probe.Map.empty ;
}
let is_computed g = g.simplified
@@ -178,9 +186,12 @@ struct
if Wp_parameters.Clean.get ()
then apply "-wp-clean" Conditions.clean g ;
end ;
- if Conditions.is_trivial g.sequent then
- g.sequent <- Conditions.trivial ;
- g.obligation <- Conditions.close g.sequent
+ begin
+ if Conditions.is_trivial g.sequent then
+ g.sequent <- Conditions.trivial ;
+ g.opened <- Conditions.property g.sequent ;
+ g.closed <- F.p_close g.opened ;
+ end
let safecompute ~pid g =
begin
@@ -191,6 +202,7 @@ struct
Wp_parameters.debug ~dkey "Simplification time: %a"
Rformat.pp_time !timer ;
g.time <- !timer ;
+ g.probes <- Conditions.probes @@ fst g.sequent ;
end
let compute ~pid g =
@@ -198,7 +210,9 @@ struct
Lang.local ~vars:(Conditions.vars_seq g.sequent)
(safecompute ~pid) g
- let compute_proof ~pid g = compute ~pid g ; g.obligation
+ let compute_proof ~pid ?(opened=false) g =
+ compute ~pid g ; if opened then g.opened else g.closed
+ let compute_probes ~pid g = compute ~pid g ; g.probes
let compute_descr ~pid g = compute ~pid g ; g.sequent
let get_descr g = g.sequent
let qed_time g = g.time
@@ -286,7 +300,9 @@ struct
if result.verdict <> NoResult then
Format.fprintf fmt "Prover %a returns %t@\n"
pp_prover prover
- (pp_result_qualif prover result)
+ (pp_result_qualif prover result) ;
+ if Wp_parameters.CounterExamples.get () then
+ pp_model fmt result.prover_model
) results ;
end
@@ -847,12 +863,6 @@ let goals_of_property prop =
in
WPOset.elements poset
-(* -------------------------------------------------------------------------- *)
-(* --- Prover and Files --- *)
-(* -------------------------------------------------------------------------- *)
-
-let get_model w = w.po_model
-
(* -------------------------------------------------------------------------- *)
(* --- Generators --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index c23d0a30f8cbe7d23adf0538c99e54cfb3235e4e..6838763a3c5c734aff5bff71246636ddc1b80c0c 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -48,8 +48,9 @@ sig
val is_computed : t -> bool
val make : Conditions.sequent -> t
val compute : pid:WpPropId.prop_id -> t -> unit
- val compute_proof : pid:WpPropId.prop_id -> t -> F.pred
+ val compute_proof : pid:WpPropId.prop_id -> ?opened:bool -> t -> F.pred
val compute_descr : pid:WpPropId.prop_id -> t -> Conditions.sequent
+ val compute_probes : pid:WpPropId.prop_id -> t -> F.term Probe.Map.t
val get_descr : t -> Conditions.sequent
val qed_time : t -> float
end