Improved congruence, implemented RP, fixed whitespace.

analyzer.ml

@@ -19,9 +19,11 @@ let doit filename = begin
   Cfg_printer.output_dot !Options.cfg_out cfg;
   let f = match !Options.domain with
 	| "signs" -> SignIterator.iterate cfg
-    | "interval" -> IntervalIterator.iterate cfg
+        | "interval" -> IntervalIterator.iterate cfg
 	| "constants" -> ConstIterator.iterate cfg
-	| _ -> ConstIterator.iterate cfg in
+	| "congruence" -> CongIterator.iterate cfg 
+	| "product" -> RPIterator.iterate cfg
+	| _ -> failwith "No valid iterator specified" in
   Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts f  end
 
 

domains/congruence.ml

@@ -1,7 +1,7 @@
 open Naked
 open Abstract_syntax_tree
 
-module Congruence : NAKED_VALUE_DOMAIN = struct
+module Congruence (*: NAKED_VALUE_DOMAIN*) = struct
   type t = { multiple : Z.t; offset : Z.t }
 
   let all_numbers = { multiple = Z.one; offset = Z.zero }
@@ -83,7 +83,9 @@ module Congruence : NAKED_VALUE_DOMAIN = struct
             offset = Z.div z1.offset z2.offset;
           }
         else all_numbers
-    | AST_MODULO -> all_numbers
+    | AST_MODULO -> if (Z.equal z2.multiple Z.zero) && (Z.divisible z1.multiple z2.offset) then
+				const (Z.rem z1.offset z2.offset)
+		    else all_numbers
 
   let compatible z = function AST_EQUAL -> z | _ -> raise NeedTop
 

domains/interval.ml

@@ -1,7 +1,7 @@
 open Naked
 open Abstract_syntax_tree
 
-module Interval : NAKED_VALUE_DOMAIN = struct
+module Interval (*: NAKED_VALUE_DOMAIN*) = struct
   type t = { lower : Z.t; upper : Z.t }
 
   let const a = { lower = a; upper = a }

domains/naked.ml

@@ -32,7 +32,7 @@ sig
 	val print: Format.formatter -> t -> unit
 end
 
-module AddTopBot (N : NAKED_VALUE_DOMAIN) : VALUE_DOMAIN = 
+module AddTopBot (N : NAKED_VALUE_DOMAIN) (*: VALUE_DOMAIN*) = 
 struct
 	type t = Bot | Top | V of N.t
 	

domains/reduced_product.ml

@@ -35,7 +35,7 @@ module ReducedProduct (C : CROSS_REDUCTION) : VALUE_DOMAIN = struct
 		(C.V.meet (fst p) (fst p')),
 		(C.W.meet (snd p) (snd p')))
 	
-	(* we do NOTC.cross-reduce p : it would not guarantee convergence anymore *)
+	(* we do NOT cross-reduce p : it would not guarantee convergence anymore *)
 	let widen p p'  = let p' = C.cr p' in C.V.widen (fst p) (fst p'), C.W.widen (snd p) (snd p')
 	let narrow p p' = let p' = C.cr p' in C.V.narrow (fst p) (fst p'), C.W.narrow (snd p) (snd p') 
 
@@ -43,5 +43,6 @@ module ReducedProduct (C : CROSS_REDUCTION) : VALUE_DOMAIN = struct
 			C.V.subset (fst p) (fst p') && C.W.subset (snd p) (snd p')
 	let is_bottom p = (C.cr p) = bottom
 	let print fmt p =
-		Format.fprintf fmt "@[<h 0>(%a, %a)@]@ " C.V.print (fst p) C.W.print (snd p)
+		Format.fprintf fmt "@[<h 0>(%a, %a)@]" C.V.print (fst p) C.W.print (snd p)
 end
+

domains/value_domain.ml

@@ -105,7 +105,7 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
 	let print out env = match env with
 		| Bot   -> Format.fprintf out "@[<h 0>Bot@]"
 		| E map -> begin Format.fprintf out "@[<h 0>{";
-				VMap.iter (fun varid val1 -> Format.fprintf out "%a : %a @ " Cfg_printer.print_var varid V.print val1) map;
+				VMap.iter (fun varid val1 -> Format.fprintf out "%a : %a@ " Cfg_printer.print_var varid V.print val1) map;
 			   Format.fprintf out "}@]"; end
 
 	let rec compute e expr = match expr with

examples/congruence/congruence.c

@@ -0,0 +1,5 @@
+void main() {
+	int x = rand(0, 10);
+	x = 2 * x;
+	assert(x % 2 == 0);
+}

examples/congruence/congruence_mul.c

@@ -0,0 +1,6 @@
+void main() {
+	int x = rand(-4,8);
+	x = 2*x;
+	x = 3*x + 2;
+	assert(x % 6 == 2);
+}

iterator/iterator.ml

@@ -93,9 +93,41 @@ open Sign
 open Constant
 open Naked
 open Value_domain
+open Congruence
+open Reduced_product
+
+module IntervalxCongr : CROSS_REDUCTION = struct
+	module V = AddTopBot(Interval)
+	module W = AddTopBot(Congruence)
+	let cr (v,w) = match v,w with
+		| _, W.Bot | V.Bot, _ -> V.Bot, W.Bot
+		| V.Top, _ | _, W.Top -> v,w
+		| V.V i, W.V c -> match c.multiple with
+			| m when Z.equal Z.zero m -> if Z.leq i.lower c.offset && Z.leq c.offset i.upper then
+					V.V {lower=c.offset; upper=c.offset}, w
+				    else
+					V.Bot, W.Bot
+			| m -> (* Non-trivial multiplier : can only hope refining the bounds *)
+				let q  = Z.div (Z.sub i.upper c.offset) m in (*rounds towards zero*)
+				let q' = Z.div (Z.sub i.lower c.offset) m in
+				if Z.equal q' q then
+					let z = Z.add c.offset (Z.mul q' m) in
+					let newint = V.const z and
+					    newmod = W.const z in newint, newmod
+				else (if Z.leq q' q then
+					let newint = V.rand (Z.add c.offset (Z.mul q' m))
+							(Z.add c.offset (Z.mul q m)) in
+					newint, w
+				else
+					V.Bot, W.Bot)
+				
+end
+
 module ConstIterator = Iterator(NonRelational(AddTopBot(Constants)))
 module SignIterator  = Iterator(NonRelational(AddTopBot(Signs)))
 module IntervalIterator  = Iterator(NonRelational(AddTopBot(Interval)))
+module CongIterator = Iterator(NonRelational(AddTopBot(Congruence)))
+module RPIterator  = Iterator(NonRelational(ReducedProduct(IntervalxCongr)))
 (*
 let  iterate cfg =
   let () = Random.self_init () in