Compare commits
No commits in common. "2808f0bd8c0ab96c7dee042d5885e5a25ad38a91" and "d838756d0e95421e1d50c1ca40a38d655d073da9" have entirely different histories.
2808f0bd8c
...
d838756d0e
5 changed files with 1 additions and 332 deletions
|
|
@ -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
|
||||
|
||||
|
|
|
|||
322
domains/karr.ml
322
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
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
void main() {
|
||||
int x = rand(0,10);
|
||||
int y = 3*x;
|
||||
assert(y == 3*x);
|
||||
}
|
||||
|
|
@ -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))
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue