analyzer.ml

@@ -23,7 +23,6 @@ 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

@@ -1,322 +0,0 @@
-open Domain
-open Cfg
-open Abstract_syntax_tree
-
-let swap arr i j =
-  let tmp = arr.(i) in
-  arr.(i) <- arr.(j);
-  arr.(j) <- tmp
-
-module Matrix : sig
-  type t
-
-  val width : t -> int
-  val height : t -> int
-  val set : t -> int -> int -> Q.t -> unit
-  val get : t -> int -> int -> Q.t
-  val init : int -> int -> (int -> int -> Q.t) -> t
-  val copy : t -> t
-  val zero : int -> int -> t
-  val is_all_zero : t -> bool
-  val map : t -> (Q.t -> Q.t) -> t
-  val neg : t -> t
-  val add : t -> t -> t
-  val sub : t -> t -> t
-  val mul : t -> t -> t
-  val linear_combine : t -> int -> int -> Q.t -> unit
-  val transpose : t -> t
-  val gauss : t * t -> t * t
-  val extend : t -> t -> t
-  val delete_line : t -> int -> t
-  val print : Format.formatter -> t -> unit
-end = struct
-  type t = { height : int; width : int; data : Q.t array array }
-
-  exception Incorrect_matrix_size
-
-  let width mat = mat.width
-  let height mat = mat.height
-
-  let set mat i j q =
-    mat.data.(i).(j) <- q;
-    ()
-
-  let get mat i j = mat.data.(i).(j)
-
-  let init n m f =
-    {
-      height = n;
-      width = m;
-      data = Array.init n (fun i -> Array.init m (fun j -> f i j));
-    }
-
-  let copy m = init m.height m.width (fun i j -> m.data.(i).(j))
-  let zero n m = init n m (fun _ _ -> Q.zero)
-
-  let is_all_zero mat =
-    Array.for_all
-      (fun a -> Array.for_all (fun elt -> Q.equal elt Q.zero) a)
-      mat.data
-
-  let map mat f = init mat.height mat.width (fun i j -> f mat.data.(i).(j))
-  let neg mat = init mat.height mat.width (fun i j -> Q.neg mat.data.(i).(j))
-
-  let add mat1 mat2 =
-    if mat1.width <> mat2.width || mat1.height <> mat2.height then
-      raise Incorrect_matrix_size
-    else
-      init mat1.height mat1.width (fun i j ->
-          Q.add mat1.data.(i).(j) mat2.data.(i).(j))
-
-  let sub mat1 mat2 = add mat1 (neg mat2)
-
-  let mul mat1 mat2 =
-    if mat1.width <> mat2.height then raise Incorrect_matrix_size
-    else
-      init mat1.height mat2.width (fun i j ->
-          List.fold_left
-            (fun sum k -> Q.add sum (Q.mul mat1.data.(i).(k) mat2.data.(k).(j)))
-            Q.zero
-            (List.init mat1.width (fun x -> x)))
-
-  let linear_combine mat line from_line coef =
-    for i = 0 to mat.width - 1 do
-      mat.data.(line).(i) <-
-        Q.add mat.data.(line).(i) (Q.mul coef mat.data.(from_line).(i))
-    done;
-    ()
-
-  let transpose mat = init mat.width mat.height (fun i j -> mat.data.(j).(i))
-
-  let gauss (m, c) =
-    let m' = copy m in
-    let c' = copy c in
-    let pivot line column =
-      let rec search_pivot l =
-        if l >= m'.height then None
-        else if not (Q.equal m'.data.(l).(column) Q.zero) then Some l
-        else search_pivot (l + 1)
-      in
-      match search_pivot line with
-      | Some pline ->
-          swap m'.data line pline;
-          swap c'.data line pline;
-          let d = m'.data.(line).(column) in
-          for i = 0 to m'.width - 1 do
-            m'.data.(line).(i) <- Q.div m'.data.(line).(i) d
-          done;
-          for i = 0 to c'.width - 1 do
-            c'.data.(line).(i) <- Q.div c'.data.(line).(i) d
-          done;
-          if line <> m'.height - 1 then
-            for l = line + 1 to m'.height - 1 do
-              linear_combine m' l line (Q.neg m'.data.(l).(column));
-              linear_combine c' l line (Q.neg m'.data.(l).(column))
-            done;
-          line + 1
-      | None -> line
-    in
-
-    if m'.height <> c'.height then raise Incorrect_matrix_size
-    else
-      let line = ref 0 in
-      for i = 0 to m'.width - 1 do
-        line := pivot !line i
-      done;
-      let m'' = init !line m'.width (fun i j -> m'.data.(i).(j)) in
-      let c'' = init !line c'.width (fun i j -> c'.data.(i).(j)) in
-      (m'', c'')
-
-  let extend mat1 mat2 =
-    if mat1.width <> mat2.width then raise Incorrect_matrix_size
-    else
-      {
-        height = mat1.height + mat2.height;
-        width = mat1.width;
-        data = Array.append mat1.data mat2.data;
-      }
-
-  let delete_line mat line =
-    if line >= mat.height then mat
-    else
-      init (mat.height - 1) mat.width (fun i j ->
-          if i < line then mat.data.(i).(j) else mat.data.(i + 1).(j))
-
-  let print fmt mat =
-    Format.pp_print_string fmt "[";
-    Array.iter
-      (fun arr ->
-        Format.pp_print_string fmt "\n";
-        Array.iter
-          (fun elt ->
-            Format.pp_print_string fmt " ";
-            Q.pp_print fmt elt)
-          arr)
-      mat.data;
-    Format.pp_print_string fmt "\n]"
-end
-
-module Karr : DOMAIN = struct
-  type t = Bot | E of Matrix.t * Matrix.t
-
-  exception Cant_assign
-
-  let init n = E (Matrix.zero 0 n, Matrix.zero 0 1)
-  let bottom = Bot
-
-  let rec explore e n =
-    match e with
-    | CFG_int_unary (unop, e') -> (
-        let v, c = explore e' n in
-        match unop with
-        | AST_UNARY_PLUS -> (v, c)
-        | AST_UNARY_MINUS -> (Matrix.neg v, Q.neg c))
-    | CFG_int_binary (binop, e', e'') -> (
-        let v', c' = explore e' n in
-        let v'', c'' = explore e'' n in
-        match binop with
-        | AST_PLUS -> (Matrix.add v' v'', Q.add c' c'')
-        | AST_MINUS -> (Matrix.sub v' v'', Q.sub c' c'')
-        | AST_MULTIPLY ->
-            if Matrix.is_all_zero v' then
-              (Matrix.map v'' (fun q -> Q.mul q c'), Q.mul c' c'')
-            else if Matrix.is_all_zero v'' then
-              (Matrix.map v' (fun q -> Q.mul q c''), Q.mul c' c'')
-            else raise Cant_assign
-        | AST_DIVIDE ->
-            if Matrix.is_all_zero v'' then
-              (Matrix.map v' (fun q -> Q.div q c''), Q.div c' c'')
-            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),
-          Q.zero )
-    | CFG_int_const const -> (Matrix.zero 1 n, Q.make const Z.one)
-    | CFG_int_rand (_, _) -> raise Cant_assign
-
-  let assign env var expr =
-    match env with
-    | Bot -> Bot
-    | E (vars, consts) -> (
-        let n = Matrix.width vars in
-        try
-          let new_line, new_const = explore expr n in
-          Matrix.set new_line 0 var.var_id
-            (Q.add (Matrix.get new_line 0 var.var_id) Q.one);
-          let new_vars = Matrix.extend vars new_line in
-          let new_consts =
-            Matrix.extend consts (Matrix.init 1 1 (fun _ _ -> new_const))
-          in
-          let v, c = Matrix.gauss (new_vars, new_consts) in
-          E (v, c)
-        with Cant_assign -> env)
-
-  let rec guard env expr =
-    match env with
-    | Bot -> Bot
-    | E (vars, consts) -> (
-        let n = Matrix.width vars in
-        let expr = rm_negations expr in
-        match expr with
-        | CFG_bool_unary (_, _) -> failwith "impossible"
-        | CFG_bool_binary (_, e, e') -> guard (guard env e) e'
-        | CFG_compare (AST_EQUAL, e, e') -> (
-            try
-              let v, c = explore (CFG_int_binary (AST_MINUS, e, e')) n in
-              E
-                ( Matrix.extend vars v,
-                  Matrix.extend consts (Matrix.init 1 1 (fun _ _ -> Q.neg c)) )
-            with Cant_assign -> env)
-        | _ -> env)
-
-  let join a b =
-    match (a, b) with
-    | Bot, x | x, Bot -> x
-    | E (vars, consts), E (vars', consts') ->
-        let av = ref (Matrix.copy vars) in
-        let ac = ref (Matrix.copy consts) in
-        let bv = ref (Matrix.copy vars') in
-        let bc = ref (Matrix.copy consts') in
-        if Matrix.width !av <> Matrix.width !bv then failwith "invalid size";
-        let n = Matrix.width !av in
-        let rec effective_join r s =
-          if s >= n then ()
-          else if
-            Q.equal (Matrix.get !av r s) Q.one
-            && Q.equal (Matrix.get !bv r s) Q.one
-          then effective_join (r + 1) (s + 1)
-          else if Q.equal (Matrix.get !av r s) Q.one then (
-            for i = 0 to r - 1 do
-              Matrix.linear_combine !av i r (Matrix.get !bv i s);
-              Matrix.linear_combine !ac i r (Matrix.get !bv i s)
-            done;
-            av := Matrix.delete_line !av r;
-            effective_join r (s + 1))
-          else if Q.equal (Matrix.get !bv r s) Q.one then (
-            for i = 0 to r - 1 do
-              Matrix.linear_combine !bv i r (Matrix.get !av i s);
-              Matrix.linear_combine !bc i r (Matrix.get !av i s)
-            done;
-            bv := Matrix.delete_line !bv r;
-            effective_join r (s + 1))
-          else if
-            r <> 0
-            && not
-                 (List.for_all
-                    (fun i -> Q.equal (Matrix.get !av i s) (Matrix.get !bv i s))
-                    (List.init r (fun x -> x)))
-          then (
-            let t = ref (-1) in
-            for i = r - 1 downto 0 do
-              if
-                !t = -1
-                && not (Q.equal (Matrix.get !av i s) (Matrix.get !bv i s))
-              then t := i
-            done;
-            let divid = Q.sub (Matrix.get !av !t s) (Matrix.get !bv !t s) in
-            for i = 0 to r - 1 do
-              let coef =
-                Q.div (Q.sub (Matrix.get !av i s) (Matrix.get !bv i s)) divid
-              in
-              Matrix.linear_combine !av i !t coef;
-              Matrix.linear_combine !ac i !t coef;
-              Matrix.linear_combine !bv i !t coef;
-              Matrix.linear_combine !bc i !t coef
-            done;
-            av := Matrix.delete_line !av !t;
-            bv := Matrix.delete_line !bv !t;
-            effective_join (r - 1) (s + 1))
-          else effective_join r (s + 1)
-        in
-        effective_join 0 0;
-        E (!av, !ac)
-
-  let meet a b =
-    match (a, b) with
-    | Bot, _ | _, Bot -> Bot
-    | E (vars, consts), E (vars', consts') ->
-        let v, c =
-          Matrix.gauss (Matrix.extend vars vars', Matrix.extend consts consts')
-        in
-        E (v, c)
-
-  let widen = join
-  let narrow = meet
-
-  let subset a b =
-    match (a, b) with
-    | Bot, _ -> true
-    | _, Bot -> false
-    | E (vars, consts), E (vars', consts') ->
-        let v = Matrix.extend vars vars' in
-        let c = Matrix.extend consts consts' in
-        let v', c' = Matrix.gauss (v, c) in
-        Matrix.is_all_zero (Matrix.sub v' vars)
-        && Matrix.is_all_zero (Matrix.sub c' consts)
-
-  let is_bottom = function Bot -> true | _ -> false
-
-  let print fmt = function
-    | Bot -> Format.pp_print_string fmt "Bot\n"
-    | E (vars, consts) -> Matrix.print fmt vars
-end

examples/karr/karr.c

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

iterator/iterator.ml

@@ -80,7 +80,6 @@ open Naked
 open Value_domain
 open Congruence
 open Reduced_product
-open Karr
 
 module IntervalxCongr : CROSS_REDUCTION = struct
 	module V = AddTopBot(Interval)
@@ -114,11 +113,10 @@ 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,7 +272,6 @@ 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