Merge branch 'fix/wp/strategies' into 'master'

[wp] fix non-terminating strategies

See merge request frama-c/frama-c!4376

src/plugins/wp/Conditions.ml

@@ -316,6 +316,9 @@ type sequent = sequence * F.pred
 
 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_false = function { seq_catg = FALSE } -> true | _ -> false

src/plugins/wp/Conditions.mli

@@ -68,6 +68,7 @@ and sequence (** List of steps *)
 type sequent = sequence * F.pred
 
 val pretty : (Format.formatter -> sequent -> unit) ref
+val equal : sequent -> sequent -> bool
 
 (** Creates a single step *)
 val step :

src/plugins/wp/Pattern.ml

@@ -40,6 +40,7 @@ and node =
   | Int of Integer.t
   | Bool of bool
   | String of string
+  | Not of ast
   | Assoc of assoc * ast list
   | Binop of ast * binop * ast
   | Call of string * ast list * bool (* trailing .. *)
@@ -48,7 +49,7 @@ and node =
   | Field of ast * string
   | Get of ast * ast
   | Set of ast * ast * ast
-and assoc = [ `Add | `Mul | `Concat | `Land | `Lor | `Lxor ]
+and assoc = [ `Add | `Mul | `Concat | `Band | `Bor | `Bxor | `And | `Or ]
 and binop = [ `Div | `Mod | `Repeat | `Eq | `Lt | `Le | `Ne | `Lsl | `Lsr ]
 
 let self p =
@@ -149,6 +150,9 @@ let rec parse ctxt p =
   | PLunop(Ubw_not,a) ->
     let a = parse ctxt a in
     { loc = a.loc ; value = Call("lf:lnot",[a],false) }
+  | PLnot a ->
+    let a = parse ctxt a in
+    { loc = a.loc ; value = Not a }
   | PLbinop(a,Bmul,b) ->
     let a = parse ctxt a in
     let b = parse ctxt b in
@@ -163,9 +167,9 @@ let rec parse ctxt p =
     let b = { loc = b.loc ; value = Times(Integer.minus_one,b) } in
     assoc `Add a b
   | PLbinop(a,Badd,b) -> assoc `Add (parse ctxt a) (parse ctxt b)
-  | PLbinop(a,Bbw_or,b) -> assoc `Lor (parse ctxt a) (parse ctxt b)
-  | PLbinop(a,Bbw_and,b) -> assoc `Land (parse ctxt a) (parse ctxt b)
-  | PLbinop(a,Bbw_xor,b) -> assoc `Lxor (parse ctxt a) (parse ctxt b)
+  | PLbinop(a,Bbw_or,b) -> assoc `Bor (parse ctxt a) (parse ctxt b)
+  | PLbinop(a,Bbw_and,b) -> assoc `Band (parse ctxt a) (parse ctxt b)
+  | PLbinop(a,Bbw_xor,b) -> assoc `Bxor (parse ctxt a) (parse ctxt b)
   | PLbinop(a,Bdiv,b) -> parse_binop ctxt ~loc `Div a b
   | PLbinop(a,Bmod,b) -> parse_binop ctxt ~loc `Mod a b
   | PLbinop(a,Blshift,b) -> parse_binop ctxt ~loc `Lsl a b
@@ -176,6 +180,8 @@ let rec parse ctxt p =
   | PLrel(a,Ge,b) -> parse_binop ctxt ~loc `Le b a
   | PLrel(a,Eq,b) -> parse_binop ctxt ~loc `Eq a b
   | PLrel(a,Neq,b) -> parse_binop ctxt ~loc `Ne a b
+  | PLand(a,b) -> assoc `And (parse ctxt a) (parse ctxt b)
+  | PLor(a,b) -> assoc `Or (parse ctxt a) (parse ctxt b)
   | PLempty -> { loc ; value = List [] }
   | PLlist ps -> { loc ; value = List (List.map (parse ctxt) ps) }
   | PLrepeat(p,n) -> parse_binop ctxt ~loc `Repeat p n
@@ -192,7 +198,7 @@ let rec parse ctxt p =
     ctxt.typing.error loc
       (if ctxt.value then "Invalid value" else "Invalid pattern")
 
-and parse_binop ctxt ~loc op a b =
+and parse_binop ctxt ~loc (op:binop) a b =
   { loc ; value = Binop(parse ctxt a,op,parse ctxt b) }
 
 let pa_pattern ctxt p = ctxt.value <- false ; parse ctxt p
@@ -211,20 +217,25 @@ let rec pp fmt (a : ast) =
   | Int n -> Integer.pretty fmt n
   | Bool b -> Format.pp_print_string fmt (if b then "\\true" else "\\false")
   | String s -> Format.fprintf fmt "%S" s
-  | Assoc(`Land,[]) -> Format.pp_print_string fmt "-1"
+  | Assoc(`Band,[]) -> Format.pp_print_string fmt "-1"
   | Assoc(`Mul,[]) -> Format.pp_print_string fmt "1"
-  | Assoc((`Add|`Lor|`Lxor),[]) -> Format.pp_print_string fmt "0"
+  | Assoc((`Add|`Bor|`Bxor),[]) -> Format.pp_print_string fmt "0"
+  | Assoc(`And,[]) -> Format.pp_print_string fmt "\\true"
+  | Assoc(`Or,[]) -> Format.pp_print_string fmt "\\false"
   | Assoc(`Concat,[]) -> Format.pp_print_string fmt "[| |]"
+  | Not a -> Format.fprintf fmt "!(%a)" pp a
   | Assoc(op,v::vs) ->
     let op = match op with
-      | `Add -> '+'
-      | `Mul -> '*'
-      | `Concat | `Lxor -> '^'
-      | `Land -> '&'
-      | `Lor -> '|'
+      | `Add -> "+"
+      | `Mul -> "*"
+      | `Concat | `Bxor -> "^"
+      | `Band -> "&"
+      | `Bor -> "|"
+      | `And -> "&&"
+      | `Or -> "||"
     in
     Format.fprintf fmt "@[<hov 2>(%a" pp v ;
-    List.iter (Format.fprintf fmt "@ %c %a" op pp) vs ;
+    List.iter (Format.fprintf fmt "@ %s %a" op pp) vs ;
     Format.fprintf fmt ")@]"
   | Binop(a,op,b) ->
     let op = match op with
@@ -313,13 +324,16 @@ let rec pmatch env (p : pattern) e =
     end
   | Bool true , True -> ()
   | Bool false , False -> ()
+  | Not p , Not e -> pmatch env p e
+  | Assoc(`Or,ps) , Or es -> pac env Lang.F.e_or [] ps es
+  | Assoc(`And,ps) , And es -> pac env Lang.F.e_and [] ps es
   | Assoc(`Add,ps) , Add es -> pac env Lang.F.e_sum [] ps es
   | Assoc(`Mul,ps) , Mul es -> pac env Lang.F.e_prod [] ps es
-  | Assoc(`Lor,ps) , Fun(lf,es) when lf == Cint.f_lor ->
+  | Assoc(`Bor,ps) , Fun(lf,es) when lf == Cint.f_lor ->
     pac env (Lang.F.e_fun lf) [] ps es
-  | Assoc(`Land,ps) , Fun(lf,es) when lf == Cint.f_land ->
+  | Assoc(`Band,ps) , Fun(lf,es) when lf == Cint.f_land ->
     pac env (Lang.F.e_fun lf) [] ps es
-  | Assoc(`Lxor,ps) , Fun(lf,es) when lf == Cint.f_lxor ->
+  | Assoc(`Bxor,ps) , Fun(lf,es) when lf == Cint.f_lxor ->
     pac env (Lang.F.e_fun lf) [] ps es
   | Binop(p,`Div,q) , Div(a,b) -> pbinop env p q a b
   | Binop(p,`Eq,q) , Div(a,b) -> pbinop env p q a b
@@ -449,10 +463,11 @@ type lookup = {
   head: bool ;
   goal: bool ;
   hyps: bool ;
+  split: bool ;
   pattern: pattern ;
 }
 
-let pclause { head ; pattern } clause sigma prop =
+let pclause { head ; pattern ; split } clause sigma prop =
   let tprop = Lang.F.e_prop prop in
   let select t =
     if t == tprop then Tactical.Clause clause else Tactical.Inside(clause,t) in
@@ -462,7 +477,7 @@ let pclause { head ; pattern } clause sigma prop =
     then Some env.sigma else None
   in
   match Lang.F.repr tprop with
-  | And ts -> plist pcond ts
+  | And ts when split -> plist pcond ts
   | _ -> pcond tprop
 
 (* --- Step Ordering --- *)
@@ -563,14 +578,17 @@ let rec select (env : sigma) (a : value) =
   | Range(a,b) -> Tactical.range a b
   | Int n -> Tactical.cint n
   | Bool b -> Tactical.compose (if b then "wp:true" else "wp:false") []
+  | Not a -> Tactical.compose "wp:not" [cc a]
   | Assoc(op,vs) ->
     let op = match op with
       | `Add -> "wp:add"
       | `Mul -> "wp:mul"
       | `Concat -> "wp:concat"
-      | `Lor -> "lf:lor"
-      | `Land -> "lf:land"
-      | `Lxor -> "lf:lxor"
+      | `And -> "wp:and"
+      | `Or -> "wp:or"
+      | `Bor -> "lf:lor"
+      | `Band -> "lf:land"
+      | `Bxor -> "lf:lxor"
     in Tactical.compose op (List.map (cc) vs)
   | Binop(a,op,b) ->
     let op = match op with
@@ -703,7 +721,10 @@ let rec typecheck env vt (a : ast) =
   | Int _ -> tc_merge ~loc vt vint
   | Bool _ -> tc_merge ~loc vt vbool
   | String _ -> tc_merge ~loc vt String
-  | Assoc((`Lor|`Land|`Lxor),vs) ->
+  | Not a -> typecheck env (tc_merge ~loc vbool vt) a
+  | Assoc((`And|`Or),vs) ->
+    List.fold_left (typecheck env) (tc_merge ~loc vbool vt) vs
+  | Assoc((`Bor|`Band|`Bxor),vs) ->
     List.fold_left (typecheck env) (tc_merge ~loc vint vt) vs
   | Assoc((`Add|`Mul),vs) ->
     List.fold_left (typecheck env) (tc_merge ~loc Numerical vt) vs

src/plugins/wp/Pattern.mli

@@ -54,6 +54,7 @@ type lookup = {
   head: bool ;
   goal: bool ;
   hyps: bool ;
+  split: bool ;
   pattern: pattern ;
 }
 

src/plugins/wp/ProofEngine.ml

@@ -150,7 +150,7 @@ let iteri f tree =
 
 let rec depth node =
   match node.parent with
-  | None -> 0
+  | None -> 1
   | Some p -> succ @@ depth p
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/ProofStrategy.ml

@@ -176,8 +176,9 @@ let parse_name ctxt ~kind ?check p =
     { loc ; value }
   | _ -> ctxt.error loc "%s name expected (%a)" kind debug p
 
-let parse_lookup penv ?(head=true) ?(goal=false) ?(hyps=false) p =
-  { goal ; hyps ; head ; pattern = Pattern.pa_pattern penv p }
+let parse_lookup penv
+    ?(head=true) ?(goal=false) ?(hyps=false) ?(split=false) p =
+  { goal ; hyps ; head ; split ; pattern = Pattern.pa_pattern penv p }
 
 let autoselect select lookup =
   match select , lookup with
@@ -208,7 +209,7 @@ let rec parse_tactic_params ctxt penv
       let lookup = List.rev_append qs lookup in
       cc ~select ~lookup ~params ~children ~default ps
     | PLapp("\\when",[],qs) ->
-      let qs = List.map (parse_lookup ~hyps:true penv) qs in
+      let qs = List.map (parse_lookup ~hyps:true ~split:true penv) qs in
       let lookup = List.rev_append qs lookup in
       cc ~select ~lookup ~params ~children ~default ps
     | PLapp("\\ingoal",[],qs) ->
@@ -216,7 +217,7 @@ let rec parse_tactic_params ctxt penv
       let lookup = List.rev_append qs lookup in
       cc ~select ~lookup ~params ~children ~default ps
     | PLapp("\\incontext",[],qs) ->
-      let qs = List.map (parse_lookup ~head:false ~hyps:true penv) qs in
+      let qs = List.map (parse_lookup ~head:false ~hyps:true ~split:true penv) qs in
       let lookup = List.rev_append qs lookup in
       cc ~select ~lookup ~params ~children ~default ps
     | PLapp("\\pattern",[],qs) ->

src/plugins/wp/ProverScript.ml

@@ -323,22 +323,39 @@ let unknown : solver = fun _ -> failed
 let (+>>) (a : solver) (b : solver) : solver =
   fun node -> a node >>= fun ok -> if ok then success else b node
 
+let progress a b =
+  let sa = ProofEngine.goal a |> Wpo.compute |> snd in
+  let sb = ProofEngine.goal b |> Wpo.compute |> snd in
+  not (Conditions.equal sa sb)
+
 let rec sequence (f : 'a -> solver) = function
   | [] -> unknown
   | x::xs -> f x +>> sequence f xs
 
+let pp_node fmt node =
+  Format.pp_print_string fmt (ProofEngine.goal node).Wpo.po_gid
+
 let rec explore_strategy env process strategy : solver =
   fun node ->
-  Wp_parameters.debug ~dkey:dkey_strategy "[%a] Strategy %s (enter)@."
-    ProofEngine.Node.pretty node (ProofStrategy.name strategy) ;
-  sequence
-    (explore_alternative env process strategy)
-    (ProofStrategy.alternatives strategy) node
-  >>= fun ok ->
-  Wp_parameters.debug ~dkey:dkey_strategy "[%a] Strategy %s: %s@."
-    ProofEngine.Node.pretty node (ProofStrategy.name strategy)
-    (if ok then "proved" else "failed");
-  Task.return ok
+  if ProofEngine.depth node > env.Env.depth then
+    begin
+      Wp_parameters.debug ~dkey:dkey_strategy "[%a] Depth limit reached (%d)"
+        pp_node node (ProofEngine.depth node) ;
+      failed
+    end
+  else
+    begin
+      Wp_parameters.debug ~dkey:dkey_strategy "[%a] Strategy %s: enter@."
+        pp_node node (ProofStrategy.name strategy) ;
+      sequence
+        (explore_alternative env process strategy)
+        (ProofStrategy.alternatives strategy) node
+      >>= fun ok ->
+      Wp_parameters.debug ~dkey:dkey_strategy "[%a] Strategy %s: %s@."
+        pp_node node (ProofStrategy.name strategy)
+        (if ok then "proved" else "failed");
+      Task.return ok
+    end
 
 and explore_alternative env process strategy alternative : solver =
   explore_provers env alternative +>>
@@ -362,13 +379,20 @@ and explore_prover env timeout prover node =
 and explore_tactic env process strategy alternative node =
   Wp_parameters.debug ~dkey:dkey_strategy
     "@[<hov 2>[%a] Trying@ %a@]"
-    ProofEngine.Node.pretty node
+    pp_node node
     ProofStrategy.pp_alternative alternative ;
   match ProofStrategy.tactic env.tree node strategy alternative with
   | None -> failed
+  | Some [node'] when not (progress node node') ->
+    Wp_parameters.debug ~dkey:dkey_strategy
+      "@[<hov 2>[%a] tactic has made no progress"
+      pp_node node ;
+    failed
   | Some nodes ->
-    Wp_parameters.debug "@[<hov 2>[%a] success (%d children)"
-      ProofEngine.Node.pretty node (List.length nodes) ;
+    Wp_parameters.debug ~dkey:dkey_strategy
+      "@[<hov 2>[%a] success (%d children) (at depth %d/%d)"
+      pp_node node (List.length nodes)
+      (ProofEngine.depth node) env.depth;
     List.iter process nodes ; success
 
 and explore_auto env process alternative node =
@@ -387,14 +411,12 @@ and explore_fallback env process alternative node =
   | Some strategy -> explore_strategy env process strategy node
 
 let explore_local_hint env process node =
-  if ProofEngine.depth node > env.Env.depth then failed
-  else
-    match ProofEngine.get_hint node with
+  match ProofEngine.get_hint node with
+  | None -> failed
+  | Some s ->
+    match ProofStrategy.find s with
     | None -> failed
-    | Some s ->
-      match ProofStrategy.find s with
-      | None -> failed
-      | Some s -> explore_strategy env process s node
+    | Some s -> explore_strategy env process s node
 
 let explore_further env process strategy node =
   let marked =

src/plugins/wp/tests/wp_tip/logical.i

+/* run.config
+   DONTRUN:
+*/
+
+/* run.config_qualif
+   OPT: -wp-status -wp-prover tip -wp-script dry
+ */
+
+/*@
+  axiomatic Observers {
+    predicate P(integer x);
+  }
+*/
+
+/*@
+  requires (x < 1000 && y < 1000 || z < 1000 && t < 1000);
+  ensures post: P(\result);
+  assigns \nothing;
+*/
+int target(unsigned x, unsigned y, unsigned z, unsigned t)
+{
+  return x+y+z+t;
+}
+/*@
+  strategy Split: \tactic("Wp.split", \pattern( (A && B) || (C && D) ));
+  proof Split: post;
+*/

src/plugins/wp/tests/wp_tip/oracle_qualif/logical.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing logical.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal target_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal target_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Valid] typed_target_assigns (Qed)
+[wp] [Unsuccess] typed_target_ensures_post (Tactic) (Qed)
+[wp] Proved goals:    3 / 4
+  Terminating:     1
+  Unreachable:     1
+  Qed:             1
+  Unsuccess:       1
+------------------------------------------------------------
+  Function target
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'target':
+Assume {
+  Type: is_uint32(t) /\ is_uint32(x) /\ is_uint32(y) /\ is_uint32(z).
+  (* Pre-condition *)
+  Have: ((t <= 999) /\ (z <= 999)) \/ ((x <= 999) /\ (y <= 999)).
+}
+Prove: P_P(to_sint32(t + to_uint32(z + to_uint32(x + y)))).
+Prover Script returns Unsuccess
+
+------------------------------------------------------------
+Subgoal 1/2:
+ - Post-condition 'post'
+ - Split (Case 1/2)
+Goal Wp.Tactical.typed_target_ensures_post-0 (generated):
+Assume {
+  Type: is_uint32(t) /\ is_uint32(x) /\ is_uint32(y) /\ is_uint32(z).
+  (* Case 1/2 *)
+  When: (t <= 999) /\ (z <= 999).
+}
+Prove: P_P(to_sint32(t + to_uint32(z + to_uint32(x + y)))).
+
+------------------------------------------------------------
+Subgoal 2/2:
+ - Post-condition 'post'
+ - Split (Case 2/2)
+Goal Wp.Tactical.typed_target_ensures_post-1 (generated):
+Assume {
+  Type: is_uint32(t) /\ is_uint32(x) /\ is_uint32(y) /\ is_uint32(z).
+  (* Case 2/2 *)
+  When: (x <= 999) /\ (y <= 999).
+}
+Prove: P_P(to_sint32(t + to_uint32(z + to_uint32(x + y)))).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  target                    1        -        2      50.0%
+------------------------------------------------------------

src/plugins/wp/tests/wp_tip/oracle_qualif/terminating.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing terminating.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Unsuccess] typed_lemma_dummy (Tactics 2) (Qed)
+[wp] Proved goals:    0 / 1
+  Unsuccess:       1
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Lemma 'dummy':
+Assume { Have: i < 0. }
+Prove: j < 0.
+Prover Alt-Ergo returns Unsuccess
+Prover Script returns Unsuccess
+
+------------------------------------------------------------
+Subgoal 1/1:
+ - Lemma 'dummy'
+ - Filter (Filter)
+ - Filter (Filter)
+Goal Wp.Tactical.typed_lemma_dummy-1 (generated):
+Prove: j < 0.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -        -        1       0.0%
+------------------------------------------------------------

src/plugins/wp/tests/wp_tip/terminating.i

+/* run.config
+   DONTRUN:
+*/
+
+/* run.config_qualif
+   OPT: -wp-status -wp-prover tip -wp-script dry
+ */
+
+/*@ lemma dummy: \forall integer i,j; i < 0 ==> j < 0; */
+
+/*@
+  strategy FastAltErgo:  \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
+  strategy EagerAltErgo: \prover("alt-ergo",10); // run Alt-Ergo for 10 sec.
+
+  strategy FilterProver:
+    FastAltErgo,
+    \tactic("Wp.filter"
+      ,\goal(_)
+      ,\children(EagerAltErgo)
+    ),
+    EagerAltErgo;
+
+  proof FilterProver: dummy;
+*/