Skip to content

Non-Apron relational domain dimchange tidyup #1754

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
DrMichaelPetter merged 6 commits into from
May 26, 2025
Merged

Non-Apron relational domain dimchange tidyup #1754

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
bbd5d8b
migrated from dimchange to dimchange2
DrMichaelPetter May 22, 2025
92f5f00
focus on reduce_col - documented matrix version and streamlined list …
DrMichaelPetter May 23, 2025
807abd0
more commentary
DrMichaelPetter May 23, 2025
ea3b0a2
disentangled change_d
DrMichaelPetter May 26, 2025
2dab048
Merge branch 'master' into dimchange-tidyup
DrMichaelPetter May 26, 2025
95fc18c
doc-commented unusual fragment
DrMichaelPetter May 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 15 additions & 15 deletions src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,18 +137,18 @@ module ArrayMatrix: ArrayMatrixFunctor =
let reduce_col_with m j =
if not @@ is_empty m then
(let r = ref (-1) in
for i' = 0 to num_rows m - 1 do
let rev_i' = num_rows m - i' - 1 in
if !r < 0 && m.(rev_i').(j) <>: A.zero then r := rev_i';
if !r <> rev_i' then
let g = m.(rev_i').(j) in
for i' = 0 to num_rows m - 1 do (* i' runs through all row indices *)
let rev_i' = num_rows m - i' - 1 in (* rev_i' runs through all row indices in reverse order *)
if !r < 0 && m.(rev_i').(j) <>: A.zero then r := rev_i'; (* if we found the j-column (non-zero element), store its row index in r *)
if !r <> rev_i' then (* exclude the non-zero element's row from the transformation *)
let g = m.(rev_i').(j) in (* only act if rev_i'/j element is non-zero*)
if g <>: A.zero then
let s = g /: m.(!r).(j) in
for j' = 0 to num_cols m - 1 do
let s = g /: m.(!r).(j) in (* determine the kill factor*)
for j' = 0 to num_cols m - 1 do (* kill the rev_i' element, eintrailing a modification of the rest columns*)
m.(rev_i').(j') <- m.(rev_i').(j') -: s *: m.(!r).(j')
done
done;
if !r >= 0 then Array.fill m.(!r) 0 (num_cols m) A.zero)
if !r >= 0 then Array.fill m.(!r) 0 (num_cols m) A.zero) (* kill row r *)

let reduce_col_with m j = timing_wrap "reduce_col_with" (reduce_col_with m) j
let reduce_col m j =
Expand All @@ -165,16 +165,16 @@ module ArrayMatrix: ArrayMatrixFunctor =

let del_cols m cols =
let n_c = Array.length cols in
if n_c = 0 || is_empty m then m
if n_c = 0 || is_empty m then m (* if #toberemoved=0, return m *)
else
let m_r, m_c = num_rows m, num_cols m in
if m_c = n_c then empty () else
let m' = Array.make_matrix m_r (m_c - n_c) A.zero in
for i = 0 to m_r - 1 do
let offset = ref 0 in
for j = 0 to (m_c - n_c) - 1 do
if m_c = n_c then empty () else (* if #cols = #toberemoved, return empty *)
let m' = Array.make_matrix m_r (m_c - n_c) A.zero in (* else alloc smaller array m' *)
for i = 0 to m_r - 1 do (* i iterates rows of m' *)
let offset = ref 0 in (* offset keeps track of coloffset *)
for j = 0 to (m_c - n_c) - 1 do (* j iterates cols of m' *)
while !offset < n_c && !offset + j = cols.(!offset) do incr offset done;
m'.(i).(j) <- m.(i).(j + !offset);
m'.(i).(j) <- m.(i).(j + !offset); (* copy m to m' *)
done
done;
m'
Expand Down
9 changes: 4 additions & 5 deletions src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,17 +186,16 @@ module ListMatrix: SparseMatrixFunctor =
let reduce_col m j =
if is_empty m then m
else
let rec find_pivot idx entries = (* Finds non-zero element in column j and returns pair of row idx and the pivot value *)
let rec find_pivot idx entries = (* Finds non-zero element in column j and returns pair of row idx, the pivot value and the row *)
match entries with
| [] -> None
| row :: rest -> let value = V.nth row j in
if value =: A.zero then find_pivot (idx - 1) rest else Some (idx, value)
if value =: A.zero then find_pivot (idx - 1) rest else Some (idx, value, row)
in
match (find_pivot (num_rows m - 1) (List.rev m)) with
| None -> m (* column is already filled with zeroes *)
| Some (row_idx, pivot) ->
let pivot_row = List.nth m row_idx in (* use the pivot row to reduce all entries in column j to zero, then "delete" the pivot row *)
List.mapi (fun idx row ->
| Some (row_idx, pivot,pivot_row) ->
List.mapi (fun idx row -> (* use the pivot row to reduce all entries in column j to zero, then "delete" the pivot row *)
if idx = row_idx then
V.zero_vec (num_cols m)
else
Expand Down
41 changes: 26 additions & 15 deletions src/cdomains/apron/affineEqualityDenseDomain.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,15 +30,14 @@ struct
let dim_add ch m = timing_wrap "dim add" (dim_add ch) m


let dim_remove (ch: Apron.Dim.change) m ~del =
let dim_remove (ch: Apron.Dim.change) m =
if Array.length ch.dim = 0 || is_empty m then
m
else (
Array.modifyi (+) ch.dim;
let m' = if not del then let m = copy m in Array.fold_left (fun y x -> reduce_col_with y x; y) m ch.dim else m in
let m' = let m = copy m in Array.fold_left (fun y x -> reduce_col_with y x; y) m ch.dim in
remove_zero_rows @@ del_cols m' ch.dim)

let dim_remove ch m ~del = timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del
let dim_remove ch m = timing_wrap "dim remove" (dim_remove ch) m
end

(** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
Expand Down Expand Up @@ -234,12 +233,11 @@ struct
let meet t1 t2 =
let sup_env = Environment.lce t1.env t2.env in

let t1, t2 = change_d t1 sup_env ~add:true ~del:false, change_d t2 sup_env ~add:true ~del:false in
let t1, t2 = dimchange2_add t1 sup_env, dimchange2_add t2 sup_env in
if is_bot t1 || is_bot t2 then
bot ()
else
(* TODO: Why can I be sure that m1 && m2 are all Some here?
Answer: because is_bot checks if t1.d is None and we checked is_bot before. *)
(* Option.get, because is_bot checks if t1.d is None and we checked is_bot before. *)
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}
Expand Down Expand Up @@ -448,22 +446,35 @@ struct
if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
res

let assign_var_parallel t vv's =
let assign_var_parallel t vv's = (* vv's is a list of pairs of lhs-variables and their rhs-values *)
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
let t = add_vars t assigned_vars in (* introduce all lhs-variables to the relation data structure *)
let primed_vars = List.init (* create a list with primed variables "i'" for each lhs-variable *)
(List.length assigned_vars)
(fun i -> Var.of_string (Int.to_string i ^"'"))
in (* TODO: we use primed integers as var names, conflict? *)
let t_primed = add_vars t primed_vars in (* introduce primed variables to the relation data structure *)
(* sequence of assignments: i' = snd vv_i : *)
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 -> (* SUBSTITUTE assigned_vars/primed_vars via OVERWRITE & ERASE *)
let replace_col m x y = (* OVERWRITES column for var_y with column for var_x *)
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 erase_cols m old_env to_erase = (* ERASES (i.e. entries are removed and column collapsed) from m all to_erase-columns *)
let m = Matrix.copy m in
let new_env = Environment.remove_vars old_env to_erase in
let dimchange = Environment.dimchange2 old_env new_env in
if Environment.equal old_env new_env then
{d = Some m; env = new_env}
else
{ d = Some (Matrix.remove_zero_rows @@ Matrix.del_cols m (Option.get dimchange.remove).dim); env=new_env}
in
let m_cp = Matrix.copy m 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 ~del:true in
let switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in (* OVERWRITE columns for assigned_vars with column for primed_vars *)
let res = erase_cols switched_m multi_t.env primed_vars in (* ERASE column for primed_vars *)
let x = Option.get res.d in
if Matrix.normalize_with x then
{d = Some x; env = res.env}
Expand Down
42 changes: 26 additions & 16 deletions src/cdomains/apron/affineEqualityDomain.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,15 +30,14 @@ struct
let dim_add ch m = timing_wrap "dim add" (dim_add ch) m


let dim_remove (ch: Apron.Dim.change) m ~del =
let dim_remove (ch: Apron.Dim.change) m =
if Array.length ch.dim = 0 || is_empty m then
m
else (
Array.modifyi (+) ch.dim;
let m' = if not del then Array.fold_left (fun y x -> reduce_col y x) m ch.dim else m in
let m' = Array.fold_left (fun y x -> reduce_col y x) m ch.dim in
remove_zero_rows @@ del_cols m' ch.dim)

let dim_remove ch m ~del = timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del
let dim_remove ch m = timing_wrap "dim remove" (dim_remove ch) m
end

(** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
Expand Down Expand Up @@ -235,12 +234,11 @@ struct
let meet t1 t2 =
let sup_env = Environment.lce t1.env t2.env in

let t1, t2 = change_d t1 sup_env ~add:true ~del:false, change_d t2 sup_env ~add:true ~del:false in
let t1, t2 = dimchange2_add t1 sup_env, dimchange2_add t2 sup_env in
if is_bot t1 || is_bot t2 then
bot ()
else
(* TODO: Why can I be sure that m1 && m2 are all Some here?
Answer: because is_bot checks if t1.d is None and we checked is_bot before. *)
(* Option.get, because is_bot checks if t1.d is None and we checked is_bot before. *)
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}
Expand Down Expand Up @@ -442,21 +440,33 @@ struct
if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
res

let assign_var_parallel t vv's =
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
let assign_var_parallel t vv's = (* vv's is a list of pairs of lhs-variables and their rhs-values *)
let assigned_vars = List.map fst vv's in
let t = add_vars t assigned_vars in (* introduce all lhs-variables to the relation data structure *)
let primed_vars = List.init (* create a list with primed variables "i'" for each lhs-variable *)
(List.length assigned_vars)
(fun i -> Var.of_string (Int.to_string i ^"'"))
in (* TODO: we use primed integers as var names, conflict? *)
let t_primed = add_vars t primed_vars in (* introduce primed variables to the relation data structure *)
(* sequence of assignments: i' = snd vv_i : *)
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 -> (* SUBSTITUTE assigned_vars/primed_vars via OVERWRITE & ERASE *)
let replace_col m x y = (* OVERWRITES column for var_y with column for var_x *)
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_upper_triangular m dim_x in
Matrix.set_col m col_x dim_y
in
let switched_m = List.fold_left2 replace_col m primed_vars assigned_vars in
let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars ~del:true in
let erase_cols m old_env to_erase = (* ERASES (i.e. entries are removed and column collapsed) from m all to_erase-columns *)
let new_env = Environment.remove_vars old_env to_erase in
let dimchange = Environment.dimchange2 old_env new_env in
if Environment.equal old_env new_env then
{d = Some m; env = new_env}
else
{ d = Some (Matrix.remove_zero_rows @@ Matrix.del_cols m (BatOption.get dimchange.remove).dim); env = new_env}
in
let switched_m = List.fold_left2 replace_col m primed_vars assigned_vars in (* OVERWRITE columns for assigned_vars with column for primed_vars *)
let res = erase_cols switched_m multi_t.env primed_vars in (* ERASE column for primed_vars *)
let x = Option.get res.d in
(match Matrix.normalize x with
| None -> bot ()
Expand Down
14 changes: 6 additions & 8 deletions src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,14 +178,12 @@ module EqualitiesConjunction = struct
if Array.length ch.dim = 0 || is_empty m then
m
else (
let cpy = Array.copy ch.dim in
Array.modifyi (+) cpy; (* this is a hack to restore the original https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html remove_dimensions semantics for dim_remove *)
let m' = Array.fold_lefti (fun y i x -> forget_variable y (x)) m cpy in (* clear m' from relations concerning ch.dim *)
modify_variables_in_domain m' cpy (-))
let m' = Array.fold_lefti (fun y i x -> forget_variable y (x)) m ch.dim in (* clear m' from relations concerning ch.dim *)
modify_variables_in_domain m' ch.dim (-))

let dim_remove ch m = Timing.wrap "dim remove" (fun m -> dim_remove ch m) m

let dim_remove ch m ~del = let res = dim_remove ch m in if M.tracing then
let dim_remove ch m = let res = dim_remove ch m in if M.tracing then
M.tracel "dim_remove" "dim remove at positions [%s] in { %s } -> { %s }"
(Array.fold_right (fun i str -> (string_of_int i) ^ ", " ^ str) ch.dim "")
(show (snd m))
Expand Down Expand Up @@ -443,8 +441,8 @@ struct

let meet t1 t2 =
let sup_env = Environment.lce t1.env t2.env in
let t1 = change_d t1 sup_env ~add:true ~del:false in
let t2 = change_d t2 sup_env ~add:true ~del:false in
let t1 = dimchange2_add t1 sup_env in
let t2 = dimchange2_add t2 sup_env in
match t1.d, t2.d with
| Some d1', Some d2' ->
EConj.IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd d2') t1 (* even on sparse d2, this will chose the relevant conjs to meet with*)
Expand Down Expand Up @@ -655,7 +653,7 @@ struct
match multi_t.d with
| Some arr when not @@ is_top multi_t ->
let switched_arr = List.fold_left2 (fun multi_t assigned_var primed_var-> assign_var multi_t assigned_var primed_var) multi_t assigned_vars primed_vars in
drop_vars switched_arr primed_vars ~del:true
remove_vars switched_arr primed_vars
| _ -> t

let assign_var_parallel t vv's =
Expand Down
Loading
Loading