[wp] fix havoc tactical

src/plugins/wp/Auto.mli

@@ -35,7 +35,7 @@ val contrapose : ?priority:float -> selection -> strategy
 val compound : ?priority:float -> selection -> strategy
 val cut : ?priority:float -> ?modus:bool -> selection -> strategy
 val filter : ?priority:float -> ?anti:bool -> unit -> strategy
-val havoc : ?priority:float -> havoc:selection -> addr:selection -> strategy
+val havoc : ?priority:float -> havoc:selection -> strategy
 val separated : ?priority:float -> selection -> strategy
 val instance : ?priority:float -> selection -> selection list -> strategy
 val lemma : ?priority:float -> ?at:selection -> string -> selection list -> strategy

src/plugins/wp/TacHavoc.ml

@@ -30,62 +30,38 @@ module L = Qed.Logic
 (* --- Havoc                                                              --- *)
 (* -------------------------------------------------------------------------- *)
 
-let field,parameter =
-  Tactical.composer
-    ~id:"address"
-    ~title:"Address"
-    ~descr:"Access Outside the Assigned Range"
-    ()
-
-let has_type t e =
-  try F.Tau.equal t (F.typeof e)
-  with Not_found -> false
-
-let match_havoc =
-  let havoc m1 = function
-    | L.Fun( f , [m_undef;m0;a;n] ) when f == MemTyped.f_havoc -> m1,(m_undef,m0,a,n)
-    | _ -> raise Not_found
-  in function
-    | L.Eq (m,m') -> (try havoc m' (F.repr m) with | Not_found -> havoc m (F.repr m'))
-    | _ -> raise Not_found
+let lookup_havoc e =
+  match F.repr e with
+  | L.Aget( m , p ) ->
+      begin
+        match F.repr m with
+        | L.Fun( f , [mr;m0;a;n] ) when f == MemTyped.f_havoc ->
+            Some( mr , m0 , a , n , p )
+        | _ -> None
+      end
+  | _ -> None
 
 class havoc =
-  object(self)
+  object
     inherit Tactical.make ~id:"Wp.havoc"
         ~title:"Havoc"
         ~descr:"Go Through Assigns"
-        ~params:[parameter]
+        ~params:[]
 
-    method select feedback sel =
-      match sel with
-      | Clause(Step s) ->
-          begin
-            match s.condition with
-            | Have p | When p ->
-                let m1,(m_undef,m0,a,n) = match_havoc (F.e_expr p) in
-                let tp = F.typeof a in
-                feedback#update_field ~filter:(has_type tp) field ;
-                let sel = self#get_field field in
-                if not (Tactical.is_empty sel) then
-                  let ptr = Tactical.selected sel in
-                  if has_type tp ptr then
-                    let separated =
-                      F.p_call MemTyped.p_separated
-                        [ ptr ; F.e_int 1 ; a ; n ] in
-                    let equal_unassigned =
-                      F.p_equal (F.e_get m1 ptr) (F.e_get m0 ptr) in
-                    let equal_assigned =
-                      F.p_equal (F.e_get m1 ptr) (F.e_get m_undef ptr) in
-                    let process = Tactical.insert ~at:s.id
-                        [ "Havoc",F.p_if separated equal_unassigned equal_assigned  ] in
-                    Applicable process
-                  else
-                    ( feedback#set_error "Not a pointer type" ;
-                      Not_configured )
-                else Not_configured
-            | _ -> Not_applicable
-          end
-      | _ -> Not_applicable
+    method select _feedback sel =
+      let at = Tactical.at sel in
+      let e = Tactical.selected sel in
+      match lookup_havoc e with
+      | None -> Not_applicable
+      | Some(mr,m0,a,n,p) ->
+          let separated =
+            F.p_call MemTyped.p_separated
+              [ p ; F.e_int 1 ; a ; n ] in
+          let process = Tactical.rewrite ?at [
+              "Unassigned" , separated , e , F.e_get m0 p ;
+              "Assigned" , F.p_not separated , e , F.e_get mr p  ;
+            ] in
+          Applicable process
   end
 
 (* -------------------------------------------------------------------------- *)
@@ -219,14 +195,13 @@ class validity =
 
 module Havoc =
 struct
-  let field = field
   let tactical = Tactical.export (new havoc)
-  let strategy ?(priority=1.0) ~havoc ~addr =
+  let strategy ?(priority=1.0) ~havoc =
     Strategy.{
       priority ;
       tactical ;
       selection = havoc ;
-      arguments = [ arg field addr ] ;
+      arguments = [] ;
     }
 end
 

src/plugins/wp/TacHavoc.mli

@@ -27,10 +27,9 @@ open Strategy
 
 module Havoc :
 sig
-  val field : selection field
   val tactical : tactical
   val strategy :
-    ?priority:float -> havoc:selection -> addr:selection -> strategy
+    ?priority:float -> havoc:selection -> strategy
 end
 
 module Separated :