From f34d1b9e52a0187f13a0a5e07c582064c7f6b2f6 Mon Sep 17 00:00:00 2001 From: soyouzpanda Date: Sat, 8 Jun 2024 23:57:48 +0200 Subject: [PATCH] Correctly renamed & began karr domain --- domains/kaar.ml | 112 ----------------------- domains/karr.ml | 236 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 236 insertions(+), 112 deletions(-) delete mode 100644 domains/kaar.ml create mode 100644 domains/karr.ml diff --git a/domains/kaar.ml b/domains/kaar.ml deleted file mode 100644 index b5eb352..0000000 --- a/domains/kaar.ml +++ /dev/null @@ -1,112 +0,0 @@ -let swap arr i j = - let tmp = arr.(i) in - arr.(i) <- arr.(j); - arr.(j) <- tmp - -module Matrix : sig - type t - - val init : int -> int -> (int -> int -> Q.t) -> t - val copy : t -> t - val zero : int -> int -> t - val neg : t -> t - val add : t -> t -> t - val sub : t -> t -> t - val mul : t -> t -> t - val transpose : t -> t - val gauss : t * t -> t * 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 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 neg mat = init mat.width mat.height (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 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 - 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 - | 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 begin - for l = line + 1 to m'.height - 1 do - sub_line l line m'.data.(l).(column) - done; - end; - 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; - (m', c') - - 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 diff --git a/domains/karr.ml b/domains/karr.ml new file mode 100644 index 0000000..11abf77 --- /dev/null +++ b/domains/karr.ml @@ -0,0 +1,236 @@ +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 transpose : t -> t + val gauss : t * t -> t * t + val extend : t -> t -> 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 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 + 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 + | 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 + sub_line l line 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 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 Kaar : 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 assign env var expr = + match env with + | Bot -> Bot + | E (vars, consts) -> ( + 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 + let new_line, new_const = explore expr 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 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