Finished Karr
This commit is contained in:
parent
f34d1b9e52
commit
0c1e540883
1 changed files with 129 additions and 43 deletions
172
domains/karr.ml
172
domains/karr.ml
|
|
@ -23,9 +23,11 @@ module Matrix : sig
|
||||||
val add : t -> t -> t
|
val add : t -> t -> t
|
||||||
val sub : t -> t -> t
|
val sub : t -> t -> t
|
||||||
val mul : t -> t -> t
|
val mul : t -> t -> t
|
||||||
|
val linear_combine : t -> int -> int -> Q.t -> unit
|
||||||
val transpose : t -> t
|
val transpose : t -> t
|
||||||
val gauss : t * t -> t * t
|
val gauss : t * t -> t * t
|
||||||
val extend : t -> t -> t
|
val extend : t -> t -> t
|
||||||
|
val delete_line : t -> int -> t
|
||||||
val print : Format.formatter -> t -> unit
|
val print : Format.formatter -> t -> unit
|
||||||
end = struct
|
end = struct
|
||||||
type t = { height : int; width : int; data : Q.t array array }
|
type t = { height : int; width : int; data : Q.t array array }
|
||||||
|
|
@ -77,6 +79,13 @@ end = struct
|
||||||
Q.zero
|
Q.zero
|
||||||
(List.init mat1.width (fun x -> x)))
|
(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 transpose mat = init mat.width mat.height (fun i j -> mat.data.(j).(i))
|
||||||
|
|
||||||
let gauss (m, c) =
|
let gauss (m, c) =
|
||||||
|
|
@ -88,14 +97,6 @@ end = struct
|
||||||
else if not (Q.equal m'.data.(l).(column) Q.zero) then Some l
|
else if not (Q.equal m'.data.(l).(column) Q.zero) then Some l
|
||||||
else search_pivot (l + 1)
|
else search_pivot (l + 1)
|
||||||
in
|
in
|
||||||
let sub_line l sl coef =
|
|
||||||
for i = 0 to m'.width - 1 do
|
|
||||||
m'.data.(l).(i) <- Q.sub m'.data.(l).(i) (Q.mul coef m'.data.(sl).(i))
|
|
||||||
done;
|
|
||||||
for i = 0 to c'.width - 1 do
|
|
||||||
c'.data.(l).(i) <- Q.sub c'.data.(l).(i) (Q.mul coef c'.data.(sl).(i))
|
|
||||||
done
|
|
||||||
in
|
|
||||||
match search_pivot line with
|
match search_pivot line with
|
||||||
| Some pline ->
|
| Some pline ->
|
||||||
swap m'.data line pline;
|
swap m'.data line pline;
|
||||||
|
|
@ -109,7 +110,8 @@ end = struct
|
||||||
done;
|
done;
|
||||||
if line <> m'.height - 1 then
|
if line <> m'.height - 1 then
|
||||||
for l = line + 1 to m'.height - 1 do
|
for l = line + 1 to m'.height - 1 do
|
||||||
sub_line l line m'.data.(l).(column)
|
linear_combine m' l line (Q.neg m'.data.(l).(column));
|
||||||
|
linear_combine c' l line (Q.neg m'.data.(l).(column))
|
||||||
done;
|
done;
|
||||||
line + 1
|
line + 1
|
||||||
| None -> line
|
| None -> line
|
||||||
|
|
@ -134,6 +136,12 @@ end = struct
|
||||||
data = Array.append mat1.data mat2.data;
|
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 =
|
let print fmt mat =
|
||||||
Format.pp_print_string fmt "[";
|
Format.pp_print_string fmt "[";
|
||||||
Array.iter
|
Array.iter
|
||||||
|
|
@ -148,7 +156,7 @@ end = struct
|
||||||
Format.pp_print_string fmt "\n]"
|
Format.pp_print_string fmt "\n]"
|
||||||
end
|
end
|
||||||
|
|
||||||
module Kaar : DOMAIN = struct
|
module Karr : DOMAIN = struct
|
||||||
type t = Bot | E of Matrix.t * Matrix.t
|
type t = Bot | E of Matrix.t * Matrix.t
|
||||||
|
|
||||||
exception Cant_assign
|
exception Cant_assign
|
||||||
|
|
@ -156,44 +164,43 @@ module Kaar : DOMAIN = struct
|
||||||
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 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 =
|
let assign env var expr =
|
||||||
match env with
|
match env with
|
||||||
| Bot -> Bot
|
| Bot -> Bot
|
||||||
| E (vars, consts) -> (
|
| E (vars, consts) -> (
|
||||||
let n = Matrix.width vars in
|
let n = Matrix.width vars in
|
||||||
let rec explore e =
|
|
||||||
match e with
|
|
||||||
| CFG_int_unary (unop, e') -> (
|
|
||||||
let v, c = explore e' 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' in
|
|
||||||
let v'', c'' = explore e'' 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
|
|
||||||
in
|
|
||||||
try
|
try
|
||||||
let new_line, new_const = explore expr in
|
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
|
||||||
(Q.add (Matrix.get new_line 0 var.var_id) Q.one);
|
(Q.add (Matrix.get new_line 0 var.var_id) Q.one);
|
||||||
let new_vars = Matrix.extend vars new_line in
|
let new_vars = Matrix.extend vars new_line in
|
||||||
|
|
@ -204,6 +211,86 @@ module Kaar : DOMAIN = struct
|
||||||
E (v, c)
|
E (v, c)
|
||||||
with Cant_assign -> env)
|
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 =
|
let meet a b =
|
||||||
match (a, b) with
|
match (a, b) with
|
||||||
| Bot, _ | _, Bot -> Bot
|
| Bot, _ | _, Bot -> Bot
|
||||||
|
|
@ -214,7 +301,6 @@ module Kaar : DOMAIN = struct
|
||||||
E (v, c)
|
E (v, c)
|
||||||
|
|
||||||
let widen = join
|
let widen = join
|
||||||
|
|
||||||
let narrow = meet
|
let narrow = meet
|
||||||
|
|
||||||
let subset a b =
|
let subset a b =
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue