From e7e4ae71f74c9efea500e0aa1b7448e4dfabddac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 4 Feb 2019 14:17:44 +0100
Subject: [PATCH] [wp] fix havoc tactical
---
src/plugins/wp/Auto.mli | 2 +-
src/plugins/wp/TacHavoc.ml | 81 +++++++++++++------------------------
src/plugins/wp/TacHavoc.mli | 3 +-
3 files changed, 30 insertions(+), 56 deletions(-)
diff --git a/src/plugins/wp/Auto.mli b/src/plugins/wp/Auto.mli
index cd8447405dc..b91ae66a573 100644
--- a/src/plugins/wp/Auto.mli
+++ b/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
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index ee2bbd7b4f0..9b7034cc308 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/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
diff --git a/src/plugins/wp/TacHavoc.mli b/src/plugins/wp/TacHavoc.mli
index 2ed3b403e08..4d25edb8d32 100644
--- a/src/plugins/wp/TacHavoc.mli
+++ b/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 :
--
GitLab