From a5d0f39537933c3a3464cb386f2f9e82c668acc7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 27 Dec 2023 18:38:06 +0100 Subject: [PATCH 01/19] Code cleanup --- .../apron/affineEqualityDomain.apron.ml | 109 +++++++++++------- 1 file changed, 69 insertions(+), 40 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 5aa1090dd4..5cd7714682 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -291,15 +291,21 @@ struct let meet t1 t2 = let sup_env = Environment.lce t1.env t2.env in - let t1, t2 = change_d t1 sup_env true false, change_d t2 sup_env true false - in if is_bot t1 || is_bot t2 then bot() else + let t1, t2 = change_d t1 sup_env true false, change_d t2 sup_env true false in + if is_bot t1 || is_bot t2 then + bot () + else + (* TODO: Why can I be sure that m1 && m2 are all Some here? *) let m1, m2 = Option.get t1.d, Option.get t2.d in - match m1, m2 with - | x, y when is_top_env t1-> {d = Some (dim_add (Environment.dimchange t2.env sup_env) y); env = sup_env} - | x, y when is_top_env t2 -> {d = Some (dim_add (Environment.dimchange t1.env sup_env) x); env = sup_env} - | x, y -> - let rref_matr = Matrix.rref_matrix_with (Matrix.copy x) (Matrix.copy y) in - if Option.is_none rref_matr then bot () else + if is_top_env t1 then + {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env} + else if is_top_env t2 then + {d = Some (dim_add (Environment.dimchange t1.env sup_env) m1); env = sup_env} + else + let rref_matr = Matrix.rref_matrix_with (Matrix.copy m1) (Matrix.copy m2) in + if Option.is_none rref_matr then + bot () + else {d = rref_matr; env = sup_env} @@ -312,12 +318,20 @@ struct let leq t1 t2 = let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *) - if env_comp = -2 || env_comp > 0 then false else - if is_bot t1 || is_top_env t2 then true else - if is_bot t2 || is_top_env t1 then false else ( + if env_comp = -2 || env_comp > 0 then + (* -2: environments are not compatible (a variable has different types in the 2 environements *) + (* -1: if env1 is a subset of env2, (OK) *) + (* 0: if equality, (OK) *) + (* +1: if env1 is a superset of env2, and +2 otherwise (the lce exists and is a strict superset of both) *) + false + else if is_bot t1 || is_top_env t2 then + true + else if is_bot t2 || is_top_env t1 then + false + else let m1, m2 = Option.get t1.d, Option.get t2.d in let m1' = if env_comp = 0 then m1 else dim_add (Environment.dimchange t1.env t2.env) m1 in - Matrix.is_covered_by m2 m1') + Matrix.is_covered_by m2 m1' let leq a b = timing_wrap "leq" (leq a) b @@ -371,7 +385,11 @@ struct lin_disjunc new_r (s + 1) new_a new_b | _ -> failwith "Matrix not in rref form" end in - if is_bot a then b else if is_bot b then a else + if is_bot a then + b + else if is_bot b then + a + else match Option.get a.d, Option.get b.d with | x, y when is_top_env a || is_top_env b -> {d = Some (Matrix.empty ()); env = Environment.lce a.env b.env} | x, y when (Environment.compare a.env b.env <> 0) -> @@ -388,33 +406,34 @@ struct let res = join a b in if M.tracing then M.tracel "join" "join a: %s b: %s -> %s \n" (show a) (show b) (show res) ; res + let widen a b = - let a_env = a.env in - let b_env = b.env in - if Environment.equal a_env b_env then + if Environment.equal a.env b.env then join a b - else b + else + b let narrow a b = a + let pretty_diff () (x, y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y - let remove_rels_with_var x var env imp = + let remove_rels_with_var x var env inplace = let j0 = Environment.dim_of_var env var in - if imp then (Matrix.reduce_col_with x j0; x) else Matrix.reduce_col x j0 + if inplace then + (Matrix.reduce_col_with x j0; x) + else + Matrix.reduce_col x j0 - let remove_rels_with_var x var env imp = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) imp + let remove_rels_with_var x var env inplace = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) inplace let forget_vars t vars = - if is_bot t || is_top_env t then t + if is_bot t || is_top_env t || List.is_empty vars then + t else let m = Option.get t.d in - if List.is_empty vars then t else - let rec rem_vars m vars' = - begin match vars' with - | [] -> m - | x :: xs -> rem_vars (remove_rels_with_var m x t.env true) xs end - in {d = Some (Matrix.remove_zero_rows @@ rem_vars (Matrix.copy m) vars); env = t.env} + let rem_from m = List.fold_left (fun m' x -> remove_rels_with_var m' x t.env true) m vars in + {d = Some (Matrix.remove_zero_rows @@ rem_from (Matrix.copy m)); env = t.env} let forget_vars t vars = let res = forget_vars t vars in @@ -472,6 +491,7 @@ struct if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s\n" (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ; res + let assign_var (t: VarManagement(Vc)(Mx).t) v v' = let t = add_vars t [v; v'] in let texpr1 = Texpr1.of_expr (t.env) (Var v') in @@ -489,14 +509,20 @@ struct let t_primed = add_vars t primed_vars in let multi_t = List.fold_left2 (fun t' v_prime (_,v') -> assign_var t' v_prime v') t_primed primed_vars vv's in match multi_t.d with - | Some m when not @@ is_top_env multi_t -> let replace_col m x y = let dim_x, dim_y = Environment.dim_of_var multi_t.env x, Environment.dim_of_var multi_t.env y in - let col_x = Matrix.get_col m dim_x in - Matrix.set_col_with m col_x dim_y in + | Some m when not @@ is_top_env multi_t -> + let replace_col m x y = + let dim_x, dim_y = Environment.dim_of_var multi_t.env x, Environment.dim_of_var multi_t.env y in + let col_x = Matrix.get_col m dim_x in + Matrix.set_col_with m col_x dim_y + in let m_cp = Matrix.copy m in - let switched_m = List.fold_left2 (fun m' x y -> replace_col m' x y) m_cp primed_vars assigned_vars in + let switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars true in let x = Option.get res.d in - if Matrix.normalize_with x then {d = Some x; env = res.env} else bot () + if Matrix.normalize_with x then + {d = Some x; env = res.env} + else + bot () | _ -> t let assign_var_parallel t vv's = @@ -561,14 +587,17 @@ struct | _, _ -> overflow_res res let meet_tcons t tcons expr = - let check_const cmp c = if cmp c Mpqf.zero then bot_env else t - in + let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in let meet_vec e = (*Flip the sign of the const. val in coeff vec*) Vector.mapi_with (fun i x -> if Vector.compare_length_with e (i + 1) = 0 then Mpqf.mone *: x else x) e; - let res = if is_bot t then bot () else - let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e - in if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} in + let res = + if is_bot t then + bot () + else + let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in + if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} + in meet_tcons_one_var_eq res expr in match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with @@ -615,9 +644,7 @@ struct let relift t = t let invariant t = - match t.d with - | None -> [] - | Some m -> + let invariant m = let earray = Lincons1.array_make t.env (Matrix.num_rows m) in for i = 0 to Lincons1.array_length earray do let row = Matrix.get_row m i in @@ -631,6 +658,8 @@ struct Lincons1.{lincons0; env = array_env} ) |> List.of_enum + in + BatOption.map_default invariant [] t.d let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1 From fe4a58f5153a7edbfae229a35d0b393d93ab93cc Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 27 Dec 2023 18:57:27 +0100 Subject: [PATCH 02/19] Fix constant printing --- .../apron/affineEqualityDomain.apron.ml | 38 +++++++++++-------- 1 file changed, 22 insertions(+), 16 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 5cd7714682..4f47f6f494 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -243,31 +243,37 @@ struct Vector.of_array @@ row in let vec_to_constraint vec env = - let vars, _ = Environment.vars env - in let dim_to_str var = - let vl = Vector.nth vec (Environment.dim_of_var env var) - in let var_str = Var.to_string var - in if vl =: Mpqf.one then "+" ^ var_str - else if vl =: Mpqf.mone then "-" ^ var_str - else if vl <: Mpqf.mone then Mpqf.to_string vl ^ var_str - else if vl >: Mpqf.one then Format.asprintf "+%s" (Mpqf.to_string vl) ^ var_str - else "" + let vars, _ = Environment.vars env in + let dim_to_str var = + let vl = Vector.nth vec (Environment.dim_of_var env var) in + let var_str = Var.to_string var in + if vl =: Mpqf.one then "+" ^ var_str + else if vl =: Mpqf.mone then "-" ^ var_str + else if vl <: Mpqf.mone then Mpqf.to_string vl ^ var_str + else if vl >: Mpqf.one then Format.asprintf "+%s" (Mpqf.to_string vl) ^ var_str + else "" in let c_to_str vl = - if vl >: Mpqf.zero then "-" ^ Mpqf.to_string vl - else if vl <: Mpqf.zero then "+" ^ Mpqf.to_string vl - else "" + if vl =: Mpqf.zero then + "" + else + let negated = vl *: Mpqf.mone in + if negated >: Mpqf.zero then "+" ^ Mpqf.to_string negated + else Mpqf.to_string negated in let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars) - ^ (c_to_str @@ Vector.nth vec (Vector.length vec - 1)) ^ "=0" - in if String.starts_with res "+" then String.sub res 1 (String.length res - 1) else res + ^ (c_to_str @@ Vector.nth vec (Vector.length vec - 1)) ^ "=0" in + if String.starts_with res "+" then + String.sub res 1 (String.length res - 1) + else + res in match t.d with | None -> "Bottom Env" | Some m when Matrix.is_empty m -> "⊤" | Some m -> - let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env) - in Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]") + let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env) in + Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]") let pretty () (x:t) = text (show x) let printXml f x = BatPrintf.fprintf f "\n\n\nmatrix\n\n\n%s\n\nenv\n\n\n%s\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env))) From 31065ed0addc6471416ae81b8b915f04dda9eb42 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 27 Dec 2023 19:47:11 +0100 Subject: [PATCH 03/19] Make computations in show directly on Z --- .../apron/affineEqualityDomain.apron.ml | 50 ++++++++++--------- 1 file changed, 26 insertions(+), 24 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 4f47f6f494..a1653bb423 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -230,39 +230,41 @@ struct let show t = let conv_to_ints row = - let module BI = IntOps.BigIntOps in - let row = Array.copy @@ Vector.to_array row - in - for i = 0 to Array.length row -1 do - let val_i = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z @@ Mpqf.get_den row.(i) - in Array.iteri(fun j x -> row.(j) <- val_i *: x) row - done; - let int_arr = Array.init (Array.length row) (fun i -> Mpqf.get_num row.(i)) - in let div = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z @@ Array.fold_left BI.gcd int_arr.(0) int_arr - in Array.iteri (fun i x -> row.(i) <- x /: div) row; - Vector.of_array @@ row + let row = Array.copy @@ Vector.to_array row in + let mpqf_of_z x = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z x in + let lcm = mpqf_of_z @@ Array.fold_left (fun x y -> Z.lcm x (Mpqf.get_den y)) Z.one row in + Array.modify (fun x -> x *: lcm) row; + let int_arr = Array.map (fun x -> Mpqf.get_num x) row in + let div = Array.fold_left Z.gcd int_arr.(0) int_arr in + Array.modify (fun x -> Z.div x div) int_arr; + int_arr in - let vec_to_constraint vec env = + let vec_to_constraint arr env = let vars, _ = Environment.vars env in let dim_to_str var = - let vl = Vector.nth vec (Environment.dim_of_var env var) in + let vl = arr.(Environment.dim_of_var env var) in let var_str = Var.to_string var in - if vl =: Mpqf.one then "+" ^ var_str - else if vl =: Mpqf.mone then "-" ^ var_str - else if vl <: Mpqf.mone then Mpqf.to_string vl ^ var_str - else if vl >: Mpqf.one then Format.asprintf "+%s" (Mpqf.to_string vl) ^ var_str - else "" + if Z.equal vl Z.zero then + "" + else if Z.equal vl Z.one then + "+" ^ var_str + else if Z.equal vl Z.minus_one then + "-" ^ var_str + else if Z.lt vl Z.minus_one then + Z.to_string vl ^ var_str + else + Format.asprintf "+%s" (Z.to_string vl) ^ var_str in - let c_to_str vl = - if vl =: Mpqf.zero then + let const_to_str vl = + if Z.equal vl Z.zero then "" else - let negated = vl *: Mpqf.mone in - if negated >: Mpqf.zero then "+" ^ Mpqf.to_string negated - else Mpqf.to_string negated + let negated = Z.mul vl Z.minus_one in + if Z.gt negated Z.zero then "+" ^ Z.to_string negated + else Z.to_string negated in let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars) - ^ (c_to_str @@ Vector.nth vec (Vector.length vec - 1)) ^ "=0" in + ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in if String.starts_with res "+" then String.sub res 1 (String.length res - 1) else From 29b8ca2f0d60e0654f83dc7b158f50064406879c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 27 Dec 2023 20:00:52 +0100 Subject: [PATCH 04/19] A bit more refactoring --- .../apron/affineEqualityDomain.apron.ml | 85 ++++++++++--------- 1 file changed, 43 insertions(+), 42 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index a1653bb423..6c5112c279 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -59,7 +59,9 @@ struct let dim_add ch m = timing_wrap "dim add" (dim_add ch) m let dim_remove (ch: Apron.Dim.change) m del = - if Array.length ch.dim = 0 || Matrix.is_empty m then m else ( + if Array.length ch.dim = 0 || Matrix.is_empty m then + m + else ( Array.iteri (fun i x-> ch.dim.(i) <- x + i) ch.dim; let m' = if not del then let m = Matrix.copy m in Array.fold_left (fun y x -> Matrix.reduce_col_with y x; y) m ch.dim else m in Matrix.remove_zero_rows @@ Matrix.del_cols m' ch.dim) @@ -146,47 +148,46 @@ struct let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*) Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0 in - let rec convert_texpr texp = - begin match texp with - (*If x is a constant, replace it with its const. val. immediately*) - | Cst x -> let of_union union = - let open Coeff in - match union with - | Interval _ -> failwith "Not a constant" - | Scalar x -> (match x with - | Float x -> Mpqf.of_float x - | Mpqf x -> x - | Mpfrf x -> Mpfr.to_mpq x) in Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x) - | Var x -> - let zero_vec_cp = Vector.copy zero_vec in - let entry_only v = Vector.set_val_with v (Environment.dim_of_var t.env x) Mpqf.one; v in - begin match t.d with - | Some m -> let row = Matrix.find_opt (fun r -> Vector.nth r (Environment.dim_of_var t.env x) =: Mpqf.one) m in - begin match row with - | Some v when is_const_vec v -> - Vector.set_val_with zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)); zero_vec_cp - | _ -> entry_only zero_vec_cp end - | None -> entry_only zero_vec_cp end - | Unop (u, e, _, _) -> - begin match u with - | Neg -> neg @@ convert_texpr e - | Cast -> convert_texpr e (*Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts*) - | Sqrt -> raise NotLinear end - | Binop (b, e1, e2, _, _) -> - begin match b with - | Add -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (convert_texpr e2); v1 - | Sub -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (neg @@ convert_texpr e2); v1 - | Mul -> - let x1, x2 = convert_texpr e1, convert_texpr e2 in - begin match get_c x1, get_c x2 with - | _, Some c -> Vector.apply_with_c_with ( *:) c x1; x1 - | Some c, _ -> Vector.apply_with_c_with ( *:) c x2; x2 - | _, _ -> raise NotLinear end - | _ -> raise NotLinear end - end - in match convert_texpr texp with - | exception NotLinear -> None - | x -> Some(x) + let rec convert_texpr = function + (*If x is a constant, replace it with its const. val. immediately*) + | Cst x -> + let of_union = function + | Coeff.Interval _ -> failwith "Not a constant" + | Scalar Float x -> Mpqf.of_float x + | Scalar Mpqf x -> x + | Scalar Mpfrf x -> Mpfr.to_mpq x + in + Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x) + | Var x -> + let zero_vec_cp = Vector.copy zero_vec in + let entry_only v = Vector.set_val_with v (Environment.dim_of_var t.env x) Mpqf.one; v in + begin match t.d with + | Some m -> + let row = Matrix.find_opt (fun r -> Vector.nth r (Environment.dim_of_var t.env x) =: Mpqf.one) m in + begin match row with + | Some v when is_const_vec v -> + Vector.set_val_with zero_vec_cp ((Vector.length zero_vec) - 1) (Vector.nth v (Vector.length v - 1)); zero_vec_cp + | _ -> entry_only zero_vec_cp + end + | None -> entry_only zero_vec_cp end + | Unop (Neg, e, _, _) -> neg @@ convert_texpr e + | Unop (Cast, e, _, _) -> convert_texpr e (*Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts*) + | Unop (Sqrt, e, _, _) -> raise NotLinear + | Binop (b, e1, e2, _, _) -> + begin match b with + | Add -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (convert_texpr e2); v1 + | Sub -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (neg @@ convert_texpr e2); v1 + | Mul -> + let x1, x2 = convert_texpr e1, convert_texpr e2 in + begin match get_c x1, get_c x2 with + | _, Some c -> Vector.apply_with_c_with ( *:) c x1; x1 + | Some c, _ -> Vector.apply_with_c_with ( *:) c x2; x2 + | _, _ -> raise NotLinear end + | _ -> raise NotLinear end + in + try + Some (convert_texpr texp) + with NotLinear -> None let get_coeff_vec t texp = timing_wrap "coeff_vec" (get_coeff_vec t) texp end From 4f113e1618883ca8a193c40e2481aab14726049e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 27 Dec 2023 20:12:36 +0100 Subject: [PATCH 05/19] Use modifyi where appropriate --- src/cdomains/apron/affineEqualityDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 6c5112c279..9febdb5778 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -53,7 +53,7 @@ struct let copy t = {t with d = Option.map Matrix.copy t.d} let dim_add (ch: Apron.Dim.change) m = - Array.iteri (fun i x -> ch.dim.(i) <- x + i) ch.dim; + Array.modifyi (fun i x -> x + i) ch.dim; (* could be written Array.modifyi (+) ch.dim; but that's too smart *) Matrix.add_empty_columns m ch.dim let dim_add ch m = timing_wrap "dim add" (dim_add ch) m @@ -62,7 +62,7 @@ struct if Array.length ch.dim = 0 || Matrix.is_empty m then m else ( - Array.iteri (fun i x-> ch.dim.(i) <- x + i) ch.dim; + Array.modifyi (fun i x -> x + i) ch.dim; let m' = if not del then let m = Matrix.copy m in Array.fold_left (fun y x -> Matrix.reduce_col_with y x; y) m ch.dim else m in Matrix.remove_zero_rows @@ Matrix.del_cols m' ch.dim) From e874d5de5aa6d65e26f1560c18bb3cb5e9c0d4f5 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 27 Dec 2023 20:26:10 +0100 Subject: [PATCH 06/19] Some formatting --- .../apron/affineEqualityDomain.apron.ml | 24 ++++++++++++------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 9febdb5778..ecd4bdc1d5 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -69,12 +69,19 @@ struct let dim_remove ch m del = timing_wrap "dim remove" (dim_remove ch m) del let change_d t new_env add del = - if Environment.equal t.env new_env then t else - let dim_change = if add then Environment.dimchange t.env new_env - else Environment.dimchange new_env t.env - in match t.d with + if Environment.equal t.env new_env then + t + else + match t.d with | None -> bot_env - | Some m -> {d = Some (if add then dim_add dim_change m else dim_remove dim_change m del); env = new_env} + | Some m -> + let dim_change = + if add then + Environment.dimchange t.env new_env + else + Environment.dimchange new_env t.env + in + {d = Some (if add then dim_add dim_change m else dim_remove dim_change m del); env = new_env} let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del @@ -133,7 +140,8 @@ struct include ConvenienceOps(Mpqf) - let get_c v = match Vector.findi (fun x -> x <>: Mpqf.zero) v with + (** Get the constant from the vector if it is a constant *) + let get_c v = match Vector.findi ((<>:) Mpqf.zero) v with | exception Not_found -> Some Mpqf.zero | i when Vector.compare_length_with v (i + 1) = 0 -> Some (Vector.nth v i) | _ -> None @@ -202,8 +210,8 @@ struct match get_coeff_vec t texpr with | Some v -> begin match get_c v with | Some c when Mpqf.get_den c = IntOps.BigIntOps.one -> - let int_val = Mpqf.get_num c - in Some int_val, Some int_val + let int_val = Mpqf.get_num c in + Some int_val, Some int_val | _ -> None, None end | _ -> None, None From 059db8d83696c5883a09dae12026a1f4595bbbbb Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 12:24:59 +0100 Subject: [PATCH 07/19] Inline Binop --- .../apron/affineEqualityDomain.apron.ml | 116 +++++++++--------- 1 file changed, 61 insertions(+), 55 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ecd4bdc1d5..fff6437882 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -59,8 +59,8 @@ struct let dim_add ch m = timing_wrap "dim add" (dim_add ch) m let dim_remove (ch: Apron.Dim.change) m del = - if Array.length ch.dim = 0 || Matrix.is_empty m then - m + if Array.length ch.dim = 0 || Matrix.is_empty m then + m else ( Array.modifyi (fun i x -> x + i) ch.dim; let m' = if not del then let m = Matrix.copy m in Array.fold_left (fun y x -> Matrix.reduce_col_with y x; y) m ch.dim else m in @@ -69,16 +69,16 @@ struct let dim_remove ch m del = timing_wrap "dim remove" (dim_remove ch m) del let change_d t new_env add del = - if Environment.equal t.env new_env then + if Environment.equal t.env new_env then t else match t.d with | None -> bot_env - | Some m -> - let dim_change = - if add then + | Some m -> + let dim_change = + if add then Environment.dimchange t.env new_env - else + else Environment.dimchange new_env t.env in {d = Some (if add then dim_add dim_change m else dim_remove dim_change m del); env = new_env} @@ -158,19 +158,19 @@ struct in let rec convert_texpr = function (*If x is a constant, replace it with its const. val. immediately*) - | Cst x -> + | Cst x -> let of_union = function | Coeff.Interval _ -> failwith "Not a constant" | Scalar Float x -> Mpqf.of_float x | Scalar Mpqf x -> x | Scalar Mpfrf x -> Mpfr.to_mpq x - in + in Vector.set_val zero_vec ((Vector.length zero_vec) - 1) (of_union x) | Var x -> let zero_vec_cp = Vector.copy zero_vec in let entry_only v = Vector.set_val_with v (Environment.dim_of_var t.env x) Mpqf.one; v in begin match t.d with - | Some m -> + | Some m -> let row = Matrix.find_opt (fun r -> Vector.nth r (Environment.dim_of_var t.env x) =: Mpqf.one) m in begin match row with | Some v when is_const_vec v -> @@ -181,18 +181,24 @@ struct | Unop (Neg, e, _, _) -> neg @@ convert_texpr e | Unop (Cast, e, _, _) -> convert_texpr e (*Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts*) | Unop (Sqrt, e, _, _) -> raise NotLinear - | Binop (b, e1, e2, _, _) -> - begin match b with - | Add -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (convert_texpr e2); v1 - | Sub -> let v1 = convert_texpr e1 in Vector.map2_with (+:) v1 (neg @@ convert_texpr e2); v1 - | Mul -> - let x1, x2 = convert_texpr e1, convert_texpr e2 in - begin match get_c x1, get_c x2 with - | _, Some c -> Vector.apply_with_c_with ( *:) c x1; x1 - | Some c, _ -> Vector.apply_with_c_with ( *:) c x2; x2 - | _, _ -> raise NotLinear end - | _ -> raise NotLinear end - in + | Binop (Add, e1, e2, _, _) -> + let v1 = convert_texpr e1 in + let v2 = convert_texpr e2 in + Vector.map2_with (+:) v1 v2; v1 + | Binop (Sub, e1, e2, _, _) -> + let v1 = convert_texpr e1 in + let v2 = convert_texpr e2 in + Vector.map2_with (+:) v1 (neg @@ v2); v1 + | Binop (Mul, e1, e2, _, _) -> + let v1 = convert_texpr e1 in + let v2 = convert_texpr e2 in + begin match get_c v1, get_c v2 with + | _, Some c -> Vector.apply_with_c_with ( *:) c v1; v1 + | Some c, _ -> Vector.apply_with_c_with ( *:) c v2; v2 + | _, _ -> raise NotLinear + end + | Binop _ -> raise NotLinear + in try Some (convert_texpr texp) with NotLinear -> None @@ -210,7 +216,7 @@ struct match get_coeff_vec t texpr with | Some v -> begin match get_c v with | Some c when Mpqf.get_den c = IntOps.BigIntOps.one -> - let int_val = Mpqf.get_num c in + let int_val = Mpqf.get_num c in Some int_val, Some int_val | _ -> None, None end | _ -> None, None @@ -249,15 +255,15 @@ struct int_arr in let vec_to_constraint arr env = - let vars, _ = Environment.vars env in + let vars, _ = Environment.vars env in let dim_to_str var = - let vl = arr.(Environment.dim_of_var env var) in - let var_str = Var.to_string var in - if Z.equal vl Z.zero then + let vl = arr.(Environment.dim_of_var env var) in + let var_str = Var.to_string var in + if Z.equal vl Z.zero then "" - else if Z.equal vl Z.one then + else if Z.equal vl Z.one then "+" ^ var_str - else if Z.equal vl Z.minus_one then + else if Z.equal vl Z.minus_one then "-" ^ var_str else if Z.lt vl Z.minus_one then Z.to_string vl ^ var_str @@ -265,7 +271,7 @@ struct Format.asprintf "+%s" (Z.to_string vl) ^ var_str in let const_to_str vl = - if Z.equal vl Z.zero then + if Z.equal vl Z.zero then "" else let negated = Z.mul vl Z.minus_one in @@ -273,8 +279,8 @@ struct else Z.to_string negated in let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars) - ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in - if String.starts_with res "+" then + ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in + if String.starts_with res "+" then String.sub res 1 (String.length res - 1) else res @@ -309,18 +315,18 @@ struct let meet t1 t2 = let sup_env = Environment.lce t1.env t2.env in let t1, t2 = change_d t1 sup_env true false, change_d t2 sup_env true false in - if is_bot t1 || is_bot t2 then + if is_bot t1 || is_bot t2 then bot () else (* TODO: Why can I be sure that m1 && m2 are all Some here? *) let m1, m2 = Option.get t1.d, Option.get t2.d in - if is_top_env t1 then - {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env} - else if is_top_env t2 then + if is_top_env t1 then + {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env} + else if is_top_env t2 then {d = Some (dim_add (Environment.dimchange t1.env sup_env) m1); env = sup_env} else let rref_matr = Matrix.rref_matrix_with (Matrix.copy m1) (Matrix.copy m2) in - if Option.is_none rref_matr then + if Option.is_none rref_matr then bot () else {d = rref_matr; env = sup_env} @@ -339,12 +345,12 @@ struct (* -2: environments are not compatible (a variable has different types in the 2 environements *) (* -1: if env1 is a subset of env2, (OK) *) (* 0: if equality, (OK) *) - (* +1: if env1 is a superset of env2, and +2 otherwise (the lce exists and is a strict superset of both) *) + (* +1: if env1 is a superset of env2, and +2 otherwise (the lce exists and is a strict superset of both) *) false - else if is_bot t1 || is_top_env t2 then + else if is_bot t1 || is_top_env t2 then true - else if is_bot t2 || is_top_env t1 then - false + else if is_bot t2 || is_top_env t1 then + false else let m1, m2 = Option.get t1.d, Option.get t2.d in let m1' = if env_comp = 0 then m1 else dim_add (Environment.dimchange t1.env t2.env) m1 in @@ -402,9 +408,9 @@ struct lin_disjunc new_r (s + 1) new_a new_b | _ -> failwith "Matrix not in rref form" end in - if is_bot a then + if is_bot a then b - else if is_bot b then + else if is_bot b then a else match Option.get a.d, Option.get b.d with @@ -437,15 +443,15 @@ struct let remove_rels_with_var x var env inplace = let j0 = Environment.dim_of_var env var in - if inplace then - (Matrix.reduce_col_with x j0; x) - else + if inplace then + (Matrix.reduce_col_with x j0; x) + else Matrix.reduce_col x j0 let remove_rels_with_var x var env inplace = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) inplace let forget_vars t vars = - if is_bot t || is_top_env t || List.is_empty vars then + if is_bot t || is_top_env t || List.is_empty vars then t else let m = Option.get t.d in @@ -526,8 +532,8 @@ struct let t_primed = add_vars t primed_vars in let multi_t = List.fold_left2 (fun t' v_prime (_,v') -> assign_var t' v_prime v') t_primed primed_vars vv's in match multi_t.d with - | Some m when not @@ is_top_env multi_t -> - let replace_col m x y = + | Some m when not @@ is_top_env multi_t -> + let replace_col m x y = let dim_x, dim_y = Environment.dim_of_var multi_t.env x, Environment.dim_of_var multi_t.env y in let col_x = Matrix.get_col m dim_x in Matrix.set_col_with m col_x dim_y @@ -536,9 +542,9 @@ struct let switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars true in let x = Option.get res.d in - if Matrix.normalize_with x then - {d = Some x; env = res.env} - else + if Matrix.normalize_with x then + {d = Some x; env = res.env} + else bot () | _ -> t @@ -609,10 +615,10 @@ struct (*Flip the sign of the const. val in coeff vec*) Vector.mapi_with (fun i x -> if Vector.compare_length_with e (i + 1) = 0 then Mpqf.mone *: x else x) e; let res = - if is_bot t then - bot () + if is_bot t then + bot () else - let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in + let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} in meet_tcons_one_var_eq res expr From 54860e74b4fc96b4d6301621df7c3ac139efe20b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 12:27:54 +0100 Subject: [PATCH 08/19] Rename `get_c` to more obvious name --- src/cdomains/apron/affineEqualityDomain.apron.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index fff6437882..82fe8fe6b6 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -141,7 +141,7 @@ struct include ConvenienceOps(Mpqf) (** Get the constant from the vector if it is a constant *) - let get_c v = match Vector.findi ((<>:) Mpqf.zero) v with + let to_constant_opt v = match Vector.findi ((<>:) Mpqf.zero) v with | exception Not_found -> Some Mpqf.zero | i when Vector.compare_length_with v (i + 1) = 0 -> Some (Vector.nth v i) | _ -> None @@ -192,7 +192,7 @@ struct | Binop (Mul, e1, e2, _, _) -> let v1 = convert_texpr e1 in let v2 = convert_texpr e2 in - begin match get_c v1, get_c v2 with + begin match to_constant_opt v1, to_constant_opt v2 with | _, Some c -> Vector.apply_with_c_with ( *:) c v1; v1 | Some c, _ -> Vector.apply_with_c_with ( *:) c v2; v2 | _, _ -> raise NotLinear @@ -214,7 +214,7 @@ struct let bound_texpr t texpr = let texpr = Texpr1.to_expr texpr in match get_coeff_vec t texpr with - | Some v -> begin match get_c v with + | Some v -> begin match to_constant_opt v with | Some c when Mpqf.get_den c = IntOps.BigIntOps.one -> let int_val = Mpqf.get_num c in Some int_val, Some int_val @@ -625,7 +625,7 @@ struct in match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with | Some v -> - begin match get_c v, Tcons1.get_typ tcons with + begin match to_constant_opt v, Tcons1.get_typ tcons with | Some c, DISEQ -> check_const (=:) c | Some c, SUP -> check_const (<=:) c | Some c, EQ -> check_const (<>:) c From f0f47987a6eb8f3d7543900610c00ab36375635c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 12:36:00 +0100 Subject: [PATCH 09/19] Simplify `bound_texpr` --- .../apron/affineEqualityDomain.apron.ml | 20 ++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 82fe8fe6b6..9ccf2294a3 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -213,20 +213,22 @@ struct let bound_texpr t texpr = let texpr = Texpr1.to_expr texpr in - match get_coeff_vec t texpr with - | Some v -> begin match to_constant_opt v with - | Some c when Mpqf.get_den c = IntOps.BigIntOps.one -> - let int_val = Mpqf.get_num c in - Some int_val, Some int_val - | _ -> None, None end + match Option.bind (get_coeff_vec t texpr) to_constant_opt with + | Some c when Mpqf.get_den c = IntOps.BigIntOps.one -> + let int_val = Mpqf.get_num c in + Some int_val, Some int_val | _ -> None, None let bound_texpr d texpr1 = let res = bound_texpr d texpr1 in - match res with - | Some min, Some max -> if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string min) (IntOps.BigIntOps.to_string max); res - | _ -> res + (if M.tracing then + match res with + | Some min, Some max -> M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string min) (IntOps.BigIntOps.to_string max) + | _ -> () + ); + res + let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 end From 44596eb2c63cb4ddfd2f3e9c86110978a2d5c361 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 12:41:14 +0100 Subject: [PATCH 10/19] Shorten function --- src/cdomains/apron/affineEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 9ccf2294a3..d2c74a82a2 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -528,7 +528,7 @@ struct res let assign_var_parallel t vv's = - let assigned_vars = List.map (function (v, _) -> v) vv's in + let assigned_vars = List.map fst vv's in let t = add_vars t assigned_vars in let primed_vars = List.init (List.length assigned_vars) (fun i -> Var.of_string (Int.to_string i ^"'")) in (* TODO: we use primed vars in analysis, conflict? *) let t_primed = add_vars t primed_vars in From b6b202ed759eb45d5ef02712a60d9685ab864509 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 12:53:42 +0100 Subject: [PATCH 11/19] Some more making things concise --- src/cdomains/apron/affineEqualityDomain.apron.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index d2c74a82a2..0bb0e856c3 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -152,7 +152,7 @@ struct let open Apron.Texpr1 in let exception NotLinear in let zero_vec = Vector.zero_vec @@ Environment.size t.env + 1 in - let neg v = Vector.map_with (fun x -> Mpqf.mone *: x) v; v in + let neg v = Vector.map_with (( *:) Mpqf.mone) v; v in let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*) Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0 in @@ -250,8 +250,8 @@ struct let row = Array.copy @@ Vector.to_array row in let mpqf_of_z x = Mpqf.of_mpz @@ Z_mlgmpidl.mpzf_of_z x in let lcm = mpqf_of_z @@ Array.fold_left (fun x y -> Z.lcm x (Mpqf.get_den y)) Z.one row in - Array.modify (fun x -> x *: lcm) row; - let int_arr = Array.map (fun x -> Mpqf.get_num x) row in + Array.modify (( *:) lcm) row; + let int_arr = Array.map Mpqf.get_num row in let div = Array.fold_left Z.gcd int_arr.(0) int_arr in Array.modify (fun x -> Z.div x div) int_arr; int_arr @@ -379,12 +379,12 @@ struct let col_a, col_b = Vector.keep_vals col_a max, Vector.keep_vals col_b max in if Vector.equal col_a col_b then (a, b, max) else let a_rev, b_rev = (Vector.rev_with col_a; col_a), (Vector.rev_with col_b; col_b) in - let i = Vector.find2i (fun x y -> x <>: y) a_rev b_rev in + let i = Vector.find2i (<>:) a_rev b_rev in let (x, y) = Vector.nth a_rev i, Vector.nth b_rev i in let r, diff = Vector.length a_rev - (i + 1), x -: y in let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in let sub_col = - Vector.map2_with (fun x y -> x -: y) a_rev b_rev; + Vector.map2_with (-:) a_rev b_rev; Vector.rev_with a_rev; a_rev in @@ -581,8 +581,8 @@ struct forget_vars res [var] let substitute_exp t var exp ov = - let res = substitute_exp t var exp ov - in if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s\n" (show t) (Var.to_string var) d_exp exp (show res); + let res = substitute_exp t var exp ov in + if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s\n" (show t) (Var.to_string var) d_exp exp (show res); res let substitute_exp t var exp ov = timing_wrap "substitution" (substitute_exp t var exp) ov From f0870881960a97a7d3afdd0f1b2f253f1c416794 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 13:00:30 +0100 Subject: [PATCH 12/19] Rename var to `coeff` --- src/cdomains/apron/affineEqualityDomain.apron.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 0bb0e856c3..5630888b59 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -259,18 +259,18 @@ struct let vec_to_constraint arr env = let vars, _ = Environment.vars env in let dim_to_str var = - let vl = arr.(Environment.dim_of_var env var) in + let coeff = arr.(Environment.dim_of_var env var) in let var_str = Var.to_string var in - if Z.equal vl Z.zero then + if Z.equal coeff Z.zero then "" - else if Z.equal vl Z.one then + else if Z.equal coeff Z.one then "+" ^ var_str - else if Z.equal vl Z.minus_one then + else if Z.equal coeff Z.minus_one then "-" ^ var_str - else if Z.lt vl Z.minus_one then - Z.to_string vl ^ var_str + else if Z.lt coeff Z.minus_one then + Z.to_string coeff ^ var_str else - Format.asprintf "+%s" (Z.to_string vl) ^ var_str + Format.asprintf "+%s" (Z.to_string coeff) ^ var_str in let const_to_str vl = if Z.equal vl Z.zero then From 0dcf8ce52ca8bd4992378ba2072a156ef68a415f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 13:04:50 +0100 Subject: [PATCH 13/19] Make show more concise --- .../apron/affineEqualityDomain.apron.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 5630888b59..7d01130480 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -260,23 +260,22 @@ struct let vars, _ = Environment.vars env in let dim_to_str var = let coeff = arr.(Environment.dim_of_var env var) in - let var_str = Var.to_string var in if Z.equal coeff Z.zero then "" - else if Z.equal coeff Z.one then - "+" ^ var_str - else if Z.equal coeff Z.minus_one then - "-" ^ var_str - else if Z.lt coeff Z.minus_one then - Z.to_string coeff ^ var_str else - Format.asprintf "+%s" (Z.to_string coeff) ^ var_str + let coeff_str = + if Z.equal coeff Z.one then "+" + else if Z.equal coeff Z.minus_one then "-" + else if Z.lt coeff Z.minus_one then Z.to_string coeff + else Format.asprintf "+%s" (Z.to_string coeff) + in + coeff_str ^ Var.to_string var in let const_to_str vl = if Z.equal vl Z.zero then "" else - let negated = Z.mul vl Z.minus_one in + let negated = Z.neg vl in if Z.gt negated Z.zero then "+" ^ Z.to_string negated else Z.to_string negated in From 399fb8c4c8fc31d91869e4851056ce0be9010b8f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 13:11:27 +0100 Subject: [PATCH 14/19] Remove code obscuring imperative nature --- .../apron/affineEqualityDomain.apron.ml | 36 ++++++++++--------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 7d01130480..2ec5dabf61 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -376,23 +376,25 @@ struct let case_three a b col_a col_b max = let col_a, col_b = Vector.copy col_a, Vector.copy col_b in let col_a, col_b = Vector.keep_vals col_a max, Vector.keep_vals col_b max in - if Vector.equal col_a col_b then (a, b, max) else - let a_rev, b_rev = (Vector.rev_with col_a; col_a), (Vector.rev_with col_b; col_b) in - let i = Vector.find2i (<>:) a_rev b_rev in - let (x, y) = Vector.nth a_rev i, Vector.nth b_rev i in - let r, diff = Vector.length a_rev - (i + 1), x -: y in - let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in - let sub_col = - Vector.map2_with (-:) a_rev b_rev; - Vector.rev_with a_rev; - a_rev - in - let multiply_by_t m t = - Matrix.map2i_with (fun i' x c -> if i' <= max then (let beta = c /: diff in - Vector.map2_with (fun u j -> u -: (beta *: j)) x t); x) m sub_col; - m - in - Matrix.remove_row (multiply_by_t a a_r) r, Matrix.remove_row (multiply_by_t b b_r) r, (max - 1) + if Vector.equal col_a col_b then + (a, b, max) + else + ( + Vector.rev_with col_a; + Vector.rev_with col_b; + let i = Vector.find2i (<>:) col_a col_b in + let (x, y) = Vector.nth col_a i, Vector.nth col_b i in + let r, diff = Vector.length col_a - (i + 1), x -: y in + let a_r, b_r = Matrix.get_row a r, Matrix.get_row b r in + Vector.map2_with (-:) col_a col_b; + Vector.rev_with col_a; + let multiply_by_t m t = + Matrix.map2i_with (fun i' x c -> if i' <= max then (let beta = c /: diff in + Vector.map2_with (fun u j -> u -: (beta *: j)) x t); x) m col_a; + m + in + Matrix.remove_row (multiply_by_t a a_r) r, Matrix.remove_row (multiply_by_t b b_r) r, (max - 1) + ) in let col_a, col_b = Matrix.get_col a s, Matrix.get_col b s in let nth_zero v i = match Vector.nth v i with From 63094e0e1fcee316a2cd8b299dd2699e3e27a193 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 13:22:08 +0100 Subject: [PATCH 15/19] Make use of `uncurry` --- src/cdomains/vectorMatrix.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/cdomains/vectorMatrix.ml b/src/cdomains/vectorMatrix.ml index d652145032..1dd684a4c0 100644 --- a/src/cdomains/vectorMatrix.ml +++ b/src/cdomains/vectorMatrix.ml @@ -251,12 +251,14 @@ module ArrayVector: AbstractVector = let nth = Array.get - let map2i f v1 v2 = let f' i (v'1, v'2) = f i v'1 v'2 in Array.mapi f' (Array.combine v1 v2) (* TODO: iter2i? *) + let map2i f v1 v2 = + let f' i = uncurry (f i) in + Array.mapi f' (Array.combine v1 v2) (* TODO: iter2i? *) let map2i_with f v1 v2 = Array.iter2i (fun i x y -> v1.(i) <- f i x y) v1 v2 - let find2i f v1 v2 = let f' (v'1, v'2) = f v'1 v'2 in - Array.findi f' (Array.combine v1 v2) (* TODO: iter2i? *) + let find2i f v1 v2 = + Array.findi (uncurry f) (Array.combine v1 v2) (* TODO: iter2i? *) let to_array v = v From 79b79d841e17fdbd273a458a0c718c78fa11a1c3 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 13:26:30 +0100 Subject: [PATCH 16/19] Simplify `meet_tcons_one_var_eq` --- .../apron/affineEqualityDomain.apron.ml | 25 +++++++++++-------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 2ec5dabf61..e05400e674 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -601,16 +601,21 @@ struct | None -> overflow_res res | Some v -> let ik = Cilfacade.get_ikind v.vtype in - match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with - | Some _, Some _ when not (Cil.isSigned ik) -> raise NotRefinable (* TODO: unsigned w/o bounds handled differently? *) - | Some min, Some max -> - assert (Z.equal min max); (* other bounds impossible in affeq *) - let (min_ik, max_ik) = IntDomain.Size.range ik in - if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then - if IntDomain.should_ignore_overflow ik then bot () else raise NotRefinable - else res - | exception Convert.Unsupported_CilExp _ - | _, _ -> overflow_res res + if not (Cil.isSigned ik) then + raise NotRefinable (* TODO: unsigned w/o bounds handled differently? *) + else + match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with + | Some min, Some max -> + assert (Z.equal min max); (* other bounds impossible in affeq *) + let (min_ik, max_ik) = IntDomain.Size.range ik in + if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then + if IntDomain.should_ignore_overflow ik then + bot () + else + raise NotRefinable + else res + | exception Convert.Unsupported_CilExp _ + | _ -> overflow_res res let meet_tcons t tcons expr = let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in From 097156f2bac7560bd92c5d4aba6babbfb6c6c152 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 13:27:51 +0100 Subject: [PATCH 17/19] Replace Z.compare with bespoke functions --- src/cdomains/apron/affineEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index e05400e674..87accda1b4 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -608,7 +608,7 @@ struct | Some min, Some max -> assert (Z.equal min max); (* other bounds impossible in affeq *) let (min_ik, max_ik) = IntDomain.Size.range ik in - if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then + if Z.lt min min_ik || Z.gt max max_ik then if IntDomain.should_ignore_overflow ik then bot () else From 0c0f3943c1d324e9e509e3edd4493592e17be8de Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Dec 2023 13:40:00 +0100 Subject: [PATCH 18/19] Some reordering & make `get_coeff_vec` more efficient --- .../apron/affineEqualityDomain.apron.ml | 54 ++++++++++--------- 1 file changed, 29 insertions(+), 25 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 87accda1b4..6f6f7c1280 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -152,7 +152,7 @@ struct let open Apron.Texpr1 in let exception NotLinear in let zero_vec = Vector.zero_vec @@ Environment.size t.env + 1 in - let neg v = Vector.map_with (( *:) Mpqf.mone) v; v in + let neg v = Vector.map_with Mpqf.neg v; v in let is_const_vec v = Vector.compare_length_with (Vector.filteri (fun i x -> (*Inefficient*) Vector.compare_length_with v (i + 1) > 0 && x <>: Mpqf.zero) v) 1 = 0 in @@ -485,7 +485,7 @@ struct let assign_invertible_rels x var b env = timing_wrap "assign_invertible" (assign_invertible_rels x var b) env in let assign_uninvertible_rel x var b env = let b_length = Vector.length b in - Vector.mapi_with (fun i z -> if i < b_length - 1 then Mpqf.mone *: z else z) b; + Vector.mapi_with (fun i z -> if i < b_length - 1 then Mpqf.neg z else z) b; Vector.set_val_with b (Environment.dim_of_var env var) Mpqf.one; let opt_m = Matrix.rref_vec_with x b in if Option.is_none opt_m then bot () else @@ -620,8 +620,9 @@ struct let meet_tcons t tcons expr = let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in let meet_vec e = - (*Flip the sign of the const. val in coeff vec*) - Vector.mapi_with (fun i x -> if Vector.compare_length_with e (i + 1) = 0 then Mpqf.mone *: x else x) e; + (* Flip the sign of the const. val in coeff vec *) + let coeff = Vector.nth e (Vector.length e - 1) in + Vector.set_val_with e (Vector.length e - 1) (Mpqf.neg coeff); let res = if is_bot t then bot () @@ -631,27 +632,30 @@ struct in meet_tcons_one_var_eq res expr in - match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with - | Some v -> - begin match to_constant_opt v, Tcons1.get_typ tcons with - | Some c, DISEQ -> check_const (=:) c - | Some c, SUP -> check_const (<=:) c - | Some c, EQ -> check_const (<>:) c - | Some c, SUPEQ -> check_const (<:) c - | None, DISEQ - | None, SUP -> - begin match meet_vec v with - | exception NotRefinable -> t - | res -> if equal res t then bot_env else t - end - | None, EQ -> - begin match meet_vec v with - | exception NotRefinable -> t - | res -> if is_bot res then bot_env else res - end - | _, _ -> t - end - | None -> t + try + match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with + | Some v -> + begin match to_constant_opt v, Tcons1.get_typ tcons with + | Some c, DISEQ -> check_const (=:) c + | Some c, SUP -> check_const (<=:) c + | Some c, EQ -> check_const (<>:) c + | Some c, SUPEQ -> check_const (<:) c + | None, DISEQ + | None, SUP -> + if equal (meet_vec v) t then + bot_env + else + t + | None, EQ -> + let res = meet_vec v in + if is_bot res then + bot_env + else + res + | _ -> t + end + | None -> t + with NotRefinable -> t let meet_tcons t tcons expr = timing_wrap "meet_tcons" (meet_tcons t tcons) expr From 3422110111c6621a85caac18db9d4412a5a01cd0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 9 Jan 2024 18:38:02 +0100 Subject: [PATCH 19/19] Rm outdated comment --- src/cdomains/apron/affineEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 6f6f7c1280..ab24515c28 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -602,7 +602,7 @@ struct | Some v -> let ik = Cilfacade.get_ikind v.vtype in if not (Cil.isSigned ik) then - raise NotRefinable (* TODO: unsigned w/o bounds handled differently? *) + raise NotRefinable else match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with | Some min, Some max ->