Selene/AStat
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Compare commits

base: Selene:d2b9ba9ae01603b7dd2dbfad2a03f0267d775f13
Branches Tags
Selene:main
Selene:elias
..
compare: Selene:498119407086ce7295855f03a140c4f3dcd03626
Branches Tags
Selene:elias
Selene:main

No commits in common. "d2b9ba9ae01603b7dd2dbfad2a03f0267d775f13" and "498119407086ce7295855f03a140c4f3dcd03626" have entirely different histories.
d2b9ba9ae0 ... 4981194070

5 changed files with 15 additions and 66 deletions
Show stats Expand all files Collapse all files

50
domains/interval.ml
View file

@ -8,8 +8,6 @@ module Interval : NAKED_VALUE_DOMAIN = struct
let rand a b = { lower = Z.min a b; upper = Z.max a b }
let infty = Z.of_int64_unsigned Int64.max_int
let min_infty = Z.neg infty
let pos = rand Z.one infty
let neg = rand min_infty Z.minus_one
let rand3 a b c =
let mi = List.fold_left Z.min a [ a; b; c ] in
@ -22,20 +20,19 @@ module Interval : NAKED_VALUE_DOMAIN = struct
rand mi ma
let minus z = rand (Z.neg z.upper) (Z.neg z.lower)
let join z1 z2 = rand4 z1.lower z2.lower z1.upper z2.upper
let meet z1 z2 =
if Z.lt z1.upper z2.lower || Z.lt z2.upper z1.lower then raise Absurd
else rand (Z.max z1.lower z2.lower) (Z.min z1.upper z2.upper)
let widen z1 z2 =
rand
(if Z.lt z1.lower z2.lower then z1.lower else min_infty)
(if Z.gt z1.upper z2.upper then z1.upper else infty)
let narrow = meet
let subset z1 z2 = Z.geq z1.lower z2.lower && Z.leq z1.upper z2.upper
let binary z1 z2 = function
| AST_PLUS -> rand (Z.add z1.lower z2.lower) (Z.add z1.upper z2.upper)
| AST_MINUS -> rand (Z.sub z1.lower z2.upper) (Z.sub z1.upper z2.lower)
@ -49,8 +46,7 @@ module Interval : NAKED_VALUE_DOMAIN = struct
rand4 (Z.div z1.lower z2.lower) (Z.div z1.upper z2.lower)
(Z.div z1.lower z2.upper) (Z.div z1.upper z2.upper)
| AST_MODULO ->
if Z.sign z2.lower <> Z.sign z2.upper || Z.sign z2.lower = 0 then
raise Absurd
if Z.sign z2.lower <> Z.sign z2.upper || Z.sign z2.lower = 0 then raise Absurd
else
rand4 (Z.rem z1.lower z2.lower) (Z.rem z1.upper z2.lower)
(Z.rem z1.lower z2.upper) (Z.rem z1.upper z2.upper)
@ -91,7 +87,7 @@ module Interval : NAKED_VALUE_DOMAIN = struct
in
let r2 =
rand
(if Z.geq z1.lower z2.lower then Z.succ z1.lower else z2.lower)
(if Z.geq z1.lower z2.lower then Z.succ z2.lower else z1.lower)
z2.upper
in
(r1, r2)
@ -101,29 +97,8 @@ module Interval : NAKED_VALUE_DOMAIN = struct
let r1 = rand z1.lower (Z.min z1.upper z2.upper) in
let r2 = rand (Z.max z1.lower z2.lower) z2.upper in
(r1, r2)
| AST_GREATER ->
let r1, r2 = compare z2 z1 AST_LESS in
(r2, r1)
| AST_GREATER_EQUAL ->
let r1, r2 = compare z2 z1 AST_LESS_EQUAL in
(r2, r1)
let has_zero z = Z.leq z.lower Z.zero && Z.geq z.upper Z.zero
let has_one z = Z.leq z.lower Z.one && Z.geq z.upper Z.one
let has_minus_one z = Z.leq z.lower Z.minus_one && Z.geq z.upper Z.minus_one
let three_part z1 z2 op =
if has_one z2 then
if has_minus_one z2 then
let a = meet pos z2 in
let b = meet neg z2 in
join (binary z1 a op) (binary z1 b op)
else
let a = meet pos z2 in
binary z1 a op
else
let a = meet neg z2 in
binary z1 a op
| AST_GREATER -> let r1, r2 = compare z2 z1 AST_LESS in r2, r1
| AST_GREATER_EQUAL -> let r1, r2 = compare z2 z1 AST_LESS_EQUAL in r2, r1
let bwd_binary z1 z2 op r =
match op with
@ -132,21 +107,12 @@ module Interval : NAKED_VALUE_DOMAIN = struct
| AST_MINUS ->
(meet z1 (binary r z2 AST_PLUS), meet z2 (binary z1 r AST_MINUS))
| AST_MULTIPLY ->
if is_only_zero z1 || is_only_zero z2 then
if has_zero r then
z1, z2
else raise Absurd
else
let z2' = meet z2 (three_part r z1 AST_DIVIDE) in
let z1' = meet z1 (three_part r z2 AST_DIVIDE) in
if has_zero r then
( (if has_zero z1' then join z1' (const Z.zero) else z1'),
if has_zero z2' then join z2' (const Z.zero) else z2' )
else (z1', z2')
(meet z1 (binary r z2 AST_DIVIDE), meet z2 (binary r z1 AST_DIVIDE))
| AST_DIVIDE ->
(meet z1 (binary r z2 AST_MULTIPLY), meet z2 (binary z1 r AST_DIVIDE))
| AST_MODULO -> (z1, z2)
let print fmt z =
Format.pp_print_string fmt "[";
Z.pp_print fmt z.lower;

2
frontend/cfg.ml
View file

@ -179,8 +179,6 @@ and node =
node_pos: position; (* position in the source *)
mutable node_out: arc list; (* arcs with this node as source *)
mutable node_in: arc list; (* arcs with this node as destination *)
mutable widen_target : bool; (* is node a candidate for widening : either head of structured loop
or destination of goto in goto-made loop that doesn't have any widen-target *)
}
and arc =

1
frontend/cfg_printer.ml
View file

@ -231,7 +231,6 @@ let print_cfg fmt p =
List.iter (fun a -> Format.fprintf fmt "%i " a.arc_src.node_id) n.node_in;
Format.fprintf fmt "out:";
List.iter (fun a -> Format.fprintf fmt "%i " a.arc_dst.node_id) n.node_out;
if n.widen_target then Format.fprintf fmt "(widen target)";
Format.fprintf fmt "\n";
) p.cfg_nodes;
Format.fprintf fmt "\n";

18
frontend/tree_to_cfg.ml
View file

@ -36,19 +36,19 @@ let node_counter = ref 0
let nodes = ref []
(* create a new node, with a fresh identifier and accumulate into nodes *)
let create_node ?(widen_target) (pos:position) =
let create_node (pos:position) =
incr node_counter;
let node =
{ node_id = !node_counter;
node_pos = pos;
node_in = [];
node_out = [];
widen_target = match widen_target with | None -> false | Some b -> b;
}
in
nodes := node::(!nodes);
node
let arcs = ref []
let arc_counter = ref 0
@ -456,7 +456,7 @@ let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env =
let env1, before, e = bool_expr env expr in
(* entry --[before]--> entry1 *)
let entry1 = append_inst entry before in
let node_t = create_node ~widen_target:true (fst x1) in
let node_t = create_node (fst x1) in
(* entry1 --[expr]--> node_t *)
add_arc entry1 node_t (CFG_guard e);
(* entry1 --[!expr]--> node_f *)
@ -487,7 +487,7 @@ let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env =
| Some (expr,_) -> bool_expr env1 expr
in
let head1 = append_inst head before in
let node_t = create_node ~widen_target:true (fst x1) in
let node_t = create_node (fst x1) in
add_arc head1 node_t (CFG_guard e);
add_arc head1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e)));
(* increment *)
@ -550,16 +550,6 @@ and stat_list (env:env) (entry:node) (exit:node) (l:stat ext list) : env =
stat_list env1 next exit rest
(*
(* Decorate a function graph with widen targets until all loops have at least one *)
let make_widen_target (e:node) =
List.iter (fun x -> if(x.node_id = e.node_id) then x.widen_target <- true) !nodes
let rec ensure_widens (entry:node) =
type color = Unseen | Opened | Visited
let type colnode = color * node in
()
*)
(* Translate a function *)

10
iterator/iterator.ml
View file

@ -31,8 +31,7 @@ module Iterator (D : DOMAIN) = struct
let node_abst n = try( NodeMap.find n !func_state )with Not_found -> D.bottom in
let update_node n s =
let acctor = if (n.widen_target) then D.widen else D.join in
func_state := NodeMap.add n (acctor (node_abst n) s) !func_state in
func_state := NodeMap.add n (D.join s (node_abst n)) !func_state in
let rec iterate n = begin
(*Format.printf "@[<h 0> Handling node %i@]@ " n.node_id;*)
@ -41,11 +40,8 @@ module Iterator (D : DOMAIN) = struct
let l = List.filter (fun x -> Node.equal x.arc_src n) cfg.cfg_arcs in begin
List.iter (fun arc -> let s = do_inst curr_abst arc in
if D.subset s (node_abst arc.arc_dst) then ()
else (let str = if arc.arc_dst.widen_target then "widen" else "join" in
Format.printf "@[<h 0>[%i -> %i] Got node %i state %a %s %a " n.node_id arc.arc_dst.node_id arc.arc_dst.node_id
D.print (node_abst arc.arc_dst)
str
D.print s;
else (Format.printf "@[<h 0>[%i -> %i] Got node %i state %a join %a " n.node_id arc.arc_dst.node_id arc.arc_dst.node_id
D.print (node_abst arc.arc_dst) D.print s;
update_node arc.arc_dst s;
Format.printf "= %a@]@ " D.print (node_abst arc.arc_dst);
func_dirty := NodeSet.add arc.arc_dst !func_dirty)) l;