Fixed compare() mishap

domains/interval.ml

@@ -8,6 +8,8 @@ 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
@@ -20,19 +22,20 @@ 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)
@@ -46,7 +49,8 @@ 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)
@@ -87,7 +91,7 @@ module Interval : NAKED_VALUE_DOMAIN = struct
           in
           let r2 =
             rand
-              (if Z.geq z1.lower z2.lower then Z.succ z2.lower else z1.lower)
+              (if Z.geq z1.lower z2.lower then Z.succ z1.lower else z2.lower)
               z2.upper
           in
           (r1, r2)
@@ -97,8 +101,29 @@ 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 ->
-    | AST_GREATER_EQUAL -> let r1, r2 = compare z2 z1 AST_LESS_EQUAL in r2, r1
+        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
 
   let bwd_binary z1 z2 op r =
     match op with
@@ -107,12 +132,21 @@ module Interval : NAKED_VALUE_DOMAIN = struct
     | AST_MINUS ->
         (meet z1 (binary r z2 AST_PLUS), meet z2 (binary z1 r AST_MINUS))
     | AST_MULTIPLY ->
-        (meet z1 (binary r z2 AST_DIVIDE), meet z2 (binary r z1 AST_DIVIDE))
+        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')
     | 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;

frontend/cfg.ml

@@ -179,6 +179,8 @@ 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 =

frontend/cfg_printer.ml

@@ -231,6 +231,7 @@ 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";

frontend/tree_to_cfg.ml

@@ -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 (pos:position) =
+let create_node ?(widen_target) (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 (fst x1) in
+       let node_t = create_node ~widen_target:true (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 (fst x1) in
+       let node_t = create_node ~widen_target:true (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,6 +550,16 @@ 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 *)
 

iterator/iterator.ml

@@ -31,7 +31,8 @@ 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 =
-				func_state := NodeMap.add n (D.join s (node_abst n)) !func_state in
+				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
 
 			let rec iterate n = begin
 				(*Format.printf "@[<h 0> Handling node %i@]@ " n.node_id;*)
@@ -40,8 +41,11 @@ 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 (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
+						else (let str = if arc.arc_dst.widen_target then "widen" else "join" in
-							D.print (node_abst arc.arc_dst) D.print s;
+						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;
 						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;