Added congruence domain

.gitignore

@@ -1,4 +1,3 @@
-*.html
 analyzer
 results/
 _build/

domains/congruence.ml

@@ -0,0 +1,143 @@
+open Naked
+open Abstract_syntax_tree
+
+module Congruence : NAKED_VALUE_DOMAIN = struct
+  type t = { multiple : Z.t; offset : Z.t }
+
+  let all_numbers = { multiple = Z.one; offset = Z.zero }
+  let const a = { multiple = Z.zero; offset = a }
+  let rand a b = if Z.equal a b then const a else all_numbers
+  let minus z = { multiple = z.multiple; offset = Z.neg z.offset }
+  let is_only_zero z = Z.equal z.multiple Z.zero && Z.equal z.offset Z.zero
+  let has_zero z = Z.equal (Z.rem z.offset z.multiple) Z.zero
+
+  let join z1 z2 =
+    {
+      multiple =
+        Z.gcd
+          (Z.gcd z1.multiple z2.multiple)
+          (Z.abs (Z.sub z1.offset z2.offset));
+      offset = z1.offset;
+    }
+
+  let meet z1 z2 =
+    let lcm = Z.lcm z1.multiple z2.multiple in
+    let gcd = Z.gcd z1.multiple z2.multiple in
+    if Z.equal (Z.rem z1.offset gcd) (Z.rem z2.offset gcd) then
+      { multiple = lcm; offset = Z.rem z1.offset gcd }
+    else raise Absurd
+
+  let multiples_of z =
+    if is_only_zero z then z
+    else if
+      (not (Z.equal z.multiple Z.zero))
+      && Z.equal (Z.rem z.offset z.multiple) Z.zero
+    then z
+    else all_numbers
+
+  let divisors_of z = z
+  let remainders z = z
+  let convex_sym z = z
+
+  let binary z1 z2 = function
+    | AST_PLUS ->
+        {
+          multiple = Z.gcd z1.multiple z2.multiple;
+          offset = Z.add z1.offset z2.offset;
+        }
+    | AST_MINUS ->
+        {
+          multiple = Z.gcd z1.multiple z2.multiple;
+          offset = Z.sub z1.offset z2.offset;
+        }
+    | AST_MULTIPLY ->
+        {
+          multiple =
+            Z.gcd
+              (Z.gcd
+                 (Z.mul z1.multiple z2.multiple)
+                 (Z.mul z1.multiple z2.offset))
+              (Z.mul z1.offset z2.multiple);
+          offset = Z.mul z1.offset z2.offset;
+        }
+    | AST_DIVIDE ->
+        if is_only_zero z2 then raise Absurd
+        else if
+          Z.equal z2.multiple Z.zero
+          && Z.divisible z1.offset z2.offset
+          && Z.divisible z1.multiple z2.offset
+        then
+          {
+            multiple = Z.div z1.multiple (Z.abs z2.offset);
+            offset = Z.div z1.offset z2.offset;
+          }
+        else all_numbers
+    | AST_MODULO -> all_numbers
+
+  let compatible z = function AST_EQUAL -> z | _ -> raise NeedTop
+
+  let rec compare z1 z2 = function
+    | AST_EQUAL ->
+        let r = meet z1 z2 in
+        (r, r)
+    | AST_NOT_EQUAL ->
+        if
+          Z.equal z1.multiple Z.zero && Z.equal z2.multiple Z.zero
+          && Z.equal z1.offset z2.offset
+        then raise Absurd
+        else (z1, z2)
+    | AST_LESS ->
+        if
+          (not (Z.equal z1.multiple Z.zero))
+          && not (Z.equal z2.multiple Z.zero)
+          || Z.equal z1.multiple Z.zero && Z.equal z2.multiple Z.zero
+             && Z.lt z1.offset z2.offset
+        then (z1, z2)
+        else raise Absurd
+    | AST_LESS_EQUAL ->
+        if
+          (not (Z.equal z1.multiple Z.zero))
+          && not (Z.equal z2.multiple Z.zero)
+          || Z.equal z1.multiple Z.zero && Z.equal z2.multiple Z.zero
+             && Z.leq z1.offset z2.offset
+        then (z1, z2)
+        else raise Absurd
+    | 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
+    | AST_PLUS ->
+        (meet z1 (binary r z2 AST_MINUS), meet z2 (binary r z1 AST_MINUS))
+    | 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 (binary r z1 AST_DIVIDE) in
+          let z1' = meet z1 (binary 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 widen = join
+  let narrow = meet
+
+  let subset z1 z2 =
+    Z.divisible z2.multiple z1.multiple
+    && Z.equal (Z.rem z1.offset z2.multiple) (Z.rem z2.offset z2.multiple)
+
+  let print fmt z =
+    Z.pp_print fmt z.multiple;
+    Format.pp_print_string fmt "Z + ";
+    Z.pp_print fmt z.offset
+end

domains/interval.ml

@@ -91,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)

domains/value_domain.ml

@@ -158,8 +158,15 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
 
 	let rec revise_HC4 tree mapenv newval = match tree with
 		| HC4_int_unary (uop, sub, abst) -> revise_HC4 sub mapenv (V.bwd_unary (get_abst sub) uop (V.meet abst newval))
-		| HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in
-							    meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2)
+		| HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in begin
+							    Format.printf "bwd_binary \"%a%s%a = %a\" -> %a, %a@ "
+								V.print (get_abst sub1)
+								(Cfg_printer.string_of_int_binary_op bop)
+								V.print (get_abst sub2)
+								V.print (V.meet abst newval)
+								V.print (refined1)
+								V.print (refined2);
+							    meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2) end
 		| HC4_int_var (v, abst)   -> E (VMap.add v (V.meet abst newval) mapenv)
 		| HC4_int_const (z,abst)  -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv
 		| HC4_int_rand (a,b,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv
@@ -174,6 +181,13 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
 			| Bot -> Bot
 			| E mapenv ->	let hc4_1, hc4_2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in
 					let newval1, newval2 = V.compare (get_abst hc4_1) (get_abst hc4_2) cop in (
+					Format.printf "Refined comparison %a%s%a as %a%s%a@ "
+						V.print (get_abst hc4_1)
+						(Cfg_printer.string_of_compare_op cop)
+						V.print (get_abst hc4_2)
+						V.print newval1
+						(Cfg_printer.string_of_compare_op cop)
+						V.print newval2;
 					meet (revise_HC4 hc4_1 mapenv newval1) (revise_HC4 hc4_2 mapenv newval2) )
 
 	let guard env boolexp = guard_noneg env (rm_negations boolexp)

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,14 @@ 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>Got node %i state %a@]@ " arc.arc_dst.node_id D.print s;
-						update_node arc.arc_dst s; func_dirty := NodeSet.add arc.arc_dst !func_dirty)) l;
+						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;
+						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;
 				if NodeSet.is_empty !func_dirty then () else
 					iterate (NodeSet.choose !func_dirty)
 				end end in

scripts/footer.html

@@ -0,0 +1,4 @@
+</div>
+</body>
+<footer><a href="./index.html">go back to index</a></footer>
+</html>

scripts/header.html

@@ -0,0 +1,22 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="utf-8">
+    <link rel="stylesheet" type="text/css" href="../scripts/style.css">
+    <link href='https://fonts.googleapis.com/css?family=Inria Serif' rel='stylesheet'>
+    <link href='https://fonts.googleapis.com/css?family=Inria Sans' rel='stylesheet'>
+    <link href='https://fonts.googleapis.com/css?family=Ubuntu Mono' rel='stylesheet'>
+    <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/10.6.0/styles/default.min.css">
+    <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/10.6.0/highlight.min.js"></script>
+    <script>
+    // first, find all the div.code blocks
+    document.addEventListener('DOMContentLoaded', (event) => {
+      document.querySelectorAll("div.c").forEach(block => {
+      // then highlight each
+        hljs.highlightBlock(block);
+      });
+    });
+    </script>
+    <title>TITLE</title>
+</head>
+<body>

scripts/header_main.html

@@ -0,0 +1,11 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="utf-8">
+    <link rel="stylesheet" type="text/css" href="../scripts/style.css">
+    <link href='https://fonts.googleapis.com/css?family=Inria Serif' rel='stylesheet'>
+    <link href='https://fonts.googleapis.com/css?family=Inria Sans' rel='stylesheet'>
+    <link href='https://fonts.googleapis.com/css?family=Ubuntu Mono' rel='stylesheet'>
+    <title>Tests overview</title>
+</head>
+<body>

scripts/test.sh

@@ -47,9 +47,13 @@ create_file() {
   file_html="${result_folder}/${filename}.html"
   if [[ ! -e "$file_html" ]]
   then
-    # cat "scripts/header.html" > $file_html
+    cat "scripts/header.html" > $file_html
     sed -i "s@TITLE@${filename}@" $file_html
+    echo "<head>" >> $file_html
+    echo "<link rel=\"stylesheet\" href=\"../scripts/style.css\">" >> $file_html
+    echo "</head>" >> $file_html
     echo "<h1>${filename}</h1>" >> $file_html
+
     echo "<div class=\"c\">" >> $file_html
     cat $file >> $file_html
     echo "</div>" >> $file_html
@@ -61,7 +65,7 @@ create_file() {
 end_file() {
   # After the analysis the cfg.dot should correspond to the current test
   dot -Tsvg cfg.dot -o ${result_folder}/${filename}.svg
-  # cat "scripts/footer.html" >> $file_html
+  cat "scripts/footer.html" >> $file_html
 }
 
 get_nth_line() {
@@ -252,7 +256,7 @@ print_end() {
 }
 
 mkdir ${result_folder}
-# cat "scripts/header_main.html"                     > $index_html
+cat "scripts/header_main.html"                     > $index_html
 echo "<h1>Overview</h1>"                          >> $index_html
 echo "<table>"                                    >> $index_html
 total=$(find $bench -iname "*.c" | wc -l)