Fixed Karr domain

analyzer.ml

@@ -23,6 +23,7 @@ let doit filename = begin
 	| "constants" -> if !Options.disjunction then ConstDisjIterator.iterate cfg else ConstIterator.iterate cfg
 	| "congruence" ->if !Options.disjunction then  CongDisjIterator.iterate cfg else CongIterator.iterate cfg
 	| "product" -> if !Options.disjunction then RPDisjIterator.iterate cfg else RPIterator.iterate cfg
+	| "karr" -> if !Options.disjunction then KarrDisjIterator.iterate cfg else KarrIterator.iterate cfg
 	| _ -> failwith "No valid iterator specified" in
   Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts f  end
 

domains/karr.ml

@@ -161,7 +161,8 @@ module Karr : DOMAIN = struct
 
   exception Cant_assign
 
-  let init n = E (Matrix.zero 0 n, Matrix.zero 0 1)
+  let init n = 
+          E (Matrix.zero 0 n, Matrix.zero 0 1)
   let bottom = Bot
 
   let rec explore e n =
@@ -189,7 +190,7 @@ module Karr : DOMAIN = struct
             else raise Cant_assign
         | AST_MODULO -> raise Cant_assign)
     | CFG_int_var var ->
-        ( Matrix.init 1 n (fun i j -> if j = var.var_id then Q.one else Q.zero),
+        ( Matrix.init 1 n (fun i j -> if j = var.var_id - 1 then Q.one else Q.zero),
           Q.zero )
     | CFG_int_const const -> (Matrix.zero 1 n, Q.make const Z.one)
     | CFG_int_rand (_, _) -> raise Cant_assign
@@ -201,8 +202,8 @@ module Karr : DOMAIN = struct
         let n = Matrix.width vars in
         try
           let new_line, new_const = explore expr n in
-          Matrix.set new_line 0 var.var_id
+          Matrix.set new_line 0 (var.var_id - 1)
-            (Q.add (Matrix.get new_line 0 var.var_id) Q.one);
+            (Q.add (Matrix.get new_line 0 (var.var_id - 1)) Q.one);
           let new_vars = Matrix.extend vars new_line in
           let new_consts =
             Matrix.extend consts (Matrix.init 1 1 (fun _ _ -> new_const))

examples/karr/karr.c

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

iterator/iterator.ml

@@ -80,6 +80,7 @@ open Naked
 open Value_domain
 open Congruence
 open Reduced_product
+open Karr
 
 module IntervalxCongr : CROSS_REDUCTION = struct
 	module V = AddTopBot(Interval)
@@ -113,10 +114,11 @@ module SignIterator  = Iterator(SimpleIterable(NonRelational(AddTopBot(Signs))))
 module IntervalIterator  = Iterator(SimpleIterable(NonRelational(AddTopBot(Interval))))
 module CongIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Congruence))))
 module RPIterator  = Iterator(SimpleIterable(NonRelational(ReducedProduct(IntervalxCongr))))
+module KarrIterator = Iterator(SimpleIterable(Karr))
 
 module ConstDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Constants))))
 module SignDisjIterator  = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Signs))))
 module IntervalDisjIterator  = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Interval))))
 module CongDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Congruence))))
 module RPDisjIterator  = Iterator(DisjunctiveIterable(NonRelational(ReducedProduct(IntervalxCongr))))
-
+module KarrDisjIterator = Iterator(DisjunctiveIterable(Karr))

scripts/test.sh

@@ -272,6 +272,7 @@ treat_examples "interval_loop" "Interval loops" "--domain interval" ""
 treat_examples "sign" "Sign and misc." "--domain signs" ""
 treat_examples "congruence" "Congruence operations" "--domain congruence" ""
 treat_examples "disjunction" "Disjunctive analysis" "--domain congruence" ""
+treat_examples "karr" "Karr's domain" "--domain karr" ""
 echo "</table>"                                   >> $index_html
 echo "</body>"                                    >> $index_html
 echo "</html>"                                    >> $index_html