Skip to content

Loading…

Add optionnal narrowing phase #3

Merged
merged 1 commit into from

2 participants

@chambart

Add a narrowing operator to test_int.

@chambart chambart Add optionnal narrowing phase
Add a narrowing operator to test_int.
6a182c5
@thomasblanc thomasblanc merged commit 4f90c92 into thomasblanc:master
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Commits on Feb 27, 2014
  1. @chambart

    Add optionnal narrowing phase

    chambart committed
    Add a narrowing operator to test_int.
This page is out of date. Refresh to see the latest.
Showing with 96 additions and 66 deletions.
  1. +1 −0 src/analysis/tlambda_analysis.ml
  2. +26 −7 src/hgraph/fixpoint.ml
  3. +2 −0 src/hgraph/fixpoint_types.mli
  4. +1 −0 test/test_data.ml
  5. +2 −0 test/test_hgraph.ml
  6. +64 −59 test/test_int.ml
View
1 src/analysis/tlambda_analysis.ml
@@ -195,6 +195,7 @@ end
let join_list _ = List.fold_left Envs.join Envs.bottom
let abstract_init v = if v = E.inv then Envs.empty else Envs.bottom
let widening _ = Envs.widening
+ let narrowing = None
type hedge_attribute = hattr
type vertex_attribute = vattr
View
33 src/hgraph/fixpoint.ml
@@ -317,7 +317,7 @@ module Fixpoint (T:T) (M:Manager with module T := T) = struct
to_update, state
- let update_vertex state vertex =
+ let update_vertex narrowing_phase state vertex =
let pred = M.H.HedgeIntSet.elements (SG.vertex_pred' state.graph vertex) in
let hedge_opt state (i,h) =
@@ -343,9 +343,19 @@ module Fixpoint (T:T) (M:Manager with module T := T) = struct
match previous_value with
| None -> true, abstract
| Some previous_value ->
- (* if this is not the first value for this state, widen *)
- let abstract = M.widening vertex previous_value abstract in
- let propagate = not (M.is_leq vertex abstract previous_value) in
+ (* if this is not the first value for this state, accelerate *)
+ let abstract, propagate =
+ (* if we are not in the narrowing phase: widen *)
+ match narrowing_phase with
+ | None ->
+ let abstract = M.widening vertex previous_value abstract in
+ let propagate = not (M.is_leq vertex abstract previous_value) in
+ abstract, propagate
+ | Some narrow ->
+ let abstract = narrow vertex previous_value abstract in
+ let propagate = not (M.is_leq vertex previous_value abstract) in
+ abstract, propagate
+ in
propagate, abstract
in
@@ -357,7 +367,7 @@ module Fixpoint (T:T) (M:Manager with module T := T) = struct
to_update, { state with vertex_values = M.H.VertexMap.add vertex abstract state.vertex_values }
- let loop state start_vertices =
+ let loop narrowing_phase state start_vertices =
let vwq = Vwq.create () in
let hwq = Hwq.create () in
Vwq.push_set vwq start_vertices;
@@ -373,7 +383,7 @@ module Fixpoint (T:T) (M:Manager with module T := T) = struct
aux state
end
| Some v ->
- let to_update, state = update_vertex state v in
+ let to_update, state = update_vertex narrowing_phase state v in
Hwq.push_set hwq to_update;
aux state
in
@@ -387,7 +397,16 @@ module Fixpoint (T:T) (M:Manager with module T := T) = struct
(SG.make_vertex state.graph M.Stack.empty v)
set) start_vertices
M.H.VertexSet.empty in
- loop state start_vertices
+ let state = loop None state start_vertices in
+ match M.narrowing with
+ | None -> state
+ | Some _ ->
+ let vertices_set =
+ List.fold_left
+ (fun set vertex -> M.H.VertexSet.add vertex set)
+ M.H.VertexSet.empty
+ (M.H.list_vertex state.graph.SG.graph) in
+ loop M.narrowing state vertices_set
let kleene_fixpoint (graph:input_graph) start_vertices =
assert(M.H.correct graph);
View
2 src/hgraph/fixpoint_types.mli
@@ -14,6 +14,8 @@ module type Manager = sig
(* val join : vertex -> abstract -> abstract -> abstract *)
val join_list : T.vertex -> abstract list -> abstract
val widening : T.vertex -> abstract -> abstract -> abstract
+ val narrowing : (T.vertex -> abstract -> abstract -> abstract) option
+
val abstract_init : T.vertex -> abstract
type vertex_attribute
View
1 test/test_data.ml
@@ -275,6 +275,7 @@ module Manager = struct
List.fold_left Env.join Env.bottom l
let widening _ a1 a2 = Env.join a1 a2
+ let narrowing = None
let is_leq _ = Env.is_leq
View
2 test/test_hgraph.ml
@@ -288,6 +288,8 @@ module Manager = struct
let widening _ a1 a2 = Env.join a1 a2
+ let narrowing = None
+
let is_leq _ = Env.is_leq
type function_id = F.t
View
123 test/test_int.ml
@@ -1,27 +1,24 @@
open Format
module A1 = struct
- type t = (int * int) option ref
+ type t = (int * int) option
type manager = unit
- let copy x = ref (!x)
- let bottom man = ref None
- let top man = ref (Some(min_int,max_int))
- let canonical man (x:t) = match !x with
- | Some(a,b) when a>b -> x := None
- | _ -> ()
+ let bottom man = None
+ let top man = Some(min_int,max_int)
+ let canonical (x:t) = match x with
+ | Some(a,b) when a>b -> None
+ | _ -> x
+
let is_bottom man (x:t) =
- canonical man x;
- !x=None
+ x=None
let is_top man (x:t) =
- canonical man x;
- match !x with
+ match x with
| None -> false
| Some(a,b) when a>min_int || b<max_int -> false
| _ -> true
let is_leq man (x:t) y =
- canonical man x; canonical man y;
- match (!x,!y) with
+ match (x,y) with
| (None,_) -> true
| (Some _, None) -> false
| (Some(a1,b1),Some(a2,b2)) ->
@@ -30,67 +27,78 @@ module A1 = struct
r
let join man (x:t) y =
- canonical man x; canonical man y;
- match (!x,!y) with
- | (None,_) -> copy y
- | (_,None) -> copy x
+ match (x,y) with
+ | (None,_) -> y
+ | (_,None) -> x
| (Some(a1,b1),Some(a2,b2)) ->
- ref (Some((min a1 a2),(max b1 b2)))
+ canonical (Some((min a1 a2),(max b1 b2)))
+
let join_list man tx =
List.fold_left (fun res x ->
join man res x) (bottom man) tx
let widening man (x:t) y =
- canonical man x; canonical man y;
- match (!x,!y) with
- | (None,_) -> copy y
+ match (x,y) with
+ | (None,_) -> y
| (_,None) -> failwith ""
| (Some(a1,b1),Some(a2,b2)) ->
- ref (Some(
- (if a2<a1 then min_int else a2),
- (if b2>b1 then max_int else b2)))
+ canonical
+ (Some(
+ (if a2<a1 then min_int else a2),
+ (if b2>b1 then max_int else b2)))
+
+ let narrow man (x:t) y =
+ match (x,y) with
+ | (_, None) -> x
+ | (None,_) -> failwith ""
+ | (Some(a1,b1),Some(a2,b2)) ->
+ canonical (Some(
+ (if a1 = min_int then a2 else a1),
+ (if b1 = max_int then b2 else b1)))
+
let print man fmt (x:t) =
- canonical man x;
- match !x with
+ match x with
| Some(a,b) ->
if is_top man x then pp_print_string fmt "top"
else
fprintf fmt "[%i,%i]" a b
| None -> pp_print_string fmt "bot"
+
let meet man (x:t) y =
- canonical man x; canonical man y;
- match (!x,!y) with
- | (None,_) -> ref None
- | (_,None) -> ref None
+ match (x,y) with
+ | (None,_) -> None
+ | (_,None) -> None
| (Some(a1,b1),Some(a2,b2)) ->
let a = max a1 a2 in
let b = min b1 b2 in
- ref (if a>b then None else Some(a,b))
+ canonical (if a>b then None else Some(a,b))
+
let setcst man (x:t) (cst:int) =
- canonical man x;
- match !x with
+ match x with
| None -> x
- | Some(a,b) -> ref (Some(cst,cst))
+ | Some(a,b) -> canonical (Some(cst,cst))
+
let addcst man (x:t) (cst:int) =
- canonical man x;
- match !x with
+ match x with
| None -> x
- | Some(a,b) -> ref (Some(
- (if a=min_int then a else a+cst),
- (if b=max_int then b else b+cst)))
+ | Some(a,b) ->
+ canonical (Some(
+ (if a=min_int then a else a+cst),
+ (if b=max_int then b else b+cst)))
+
let leqcst man (x:t) (cst:int) =
- canonical man x;
- match !x with
+ match x with
| None -> x
| Some(a,b) ->
- let i = ref(Some(min_int,cst)) in
+ let i = canonical (Some(min_int,cst)) in
meet man (x:t) i
+
let geqcst man (x:t) (cst:int) =
- canonical man x;
- match !x with
+ match x with
| None -> x
| Some(a,b) ->
- let i = ref(Some(cst,max_int)) in
+ let i = canonical (Some(cst,max_int)) in
meet man x i
+
end
module A2 = struct
@@ -103,11 +111,6 @@ module A2 = struct
let top = A1.top man in (top,top)
let is_bottom man (x,y) =
A1.is_bottom man x || A1.is_bottom man y
- let canonical man ((x,y) as abs) =
- A1.canonical man x; A1.canonical man y;
- if is_bottom man abs then begin
- x := None; y := None
- end
let is_leq man (x1,y1) (x2,y2) =
A1.is_leq man x1 x2 && A1.is_leq man y1 y2
let join man (x1,y1) (x2,y2) =
@@ -117,8 +120,10 @@ module A2 = struct
join man res x) (bottom man) tx
let widening man (x1,y1) (x2,y2) =
(A1.widening man x1 x2, A1.widening man y1 y2)
+ let narrow man (x1,y1) (x2,y2) =
+ (A1.narrow man x1 x2, A1.narrow man y1 y2)
+ let narrowing = Some narrow
let print man fmt ((x,y) as v) =
- canonical man v;
if is_bottom man v then pp_print_string fmt "bot"
else fprintf fmt "(%a,%a)" (A1.print man) x (A1.print man) y
let meet man (x1,y1) (x2,y2) =
@@ -126,8 +131,8 @@ module A2 = struct
let setcst man ((x,y) as v) (dim:int) (cst:int) =
if is_bottom man v
then v
- else if dim=0 then (A1.setcst man x cst, A1.copy y)
- else if dim=1 then (A1.copy x, A1.setcst man y cst)
+ else if dim=0 then (A1.setcst man x cst, y)
+ else if dim=1 then (x, A1.setcst man y cst)
else failwith ""
let assignvar man ((x,y) as v) (dim1:int) (dim2:int) =
@@ -140,20 +145,20 @@ module A2 = struct
let addcst man ((x,y) as v) (dim:int) (cst:int) =
if is_bottom man v || cst==0
then v
- else if dim=0 then (A1.addcst man x cst, A1.copy y)
- else if dim=1 then (A1.copy x, A1.addcst man y cst)
+ else if dim=0 then (A1.addcst man x cst, y)
+ else if dim=1 then (x, A1.addcst man y cst)
else failwith ""
let leqcst man ((x,y) as v) (dim:int) (cst:int) =
if is_bottom man v
then v
- else if dim=0 then (A1.leqcst man x cst, A1.copy y)
- else if dim=1 then (A1.copy x, A1.leqcst man y cst)
+ else if dim=0 then (A1.leqcst man x cst, y)
+ else if dim=1 then (x, A1.leqcst man y cst)
else failwith ""
let geqcst man ((x,y) as v) (dim:int) (cst:int) =
if is_bottom man v
then v
- else if dim=0 then (A1.geqcst man x cst, A1.copy y)
- else if dim=1 then (A1.copy x, A1.geqcst man y cst)
+ else if dim=0 then (A1.geqcst man x cst, y)
+ else if dim=1 then (x, A1.geqcst man y cst)
else failwith ""
end
Something went wrong with that request. Please try again.