Skip to content

VSD - max array length #6293

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
merged 14 commits into from
Aug 14, 2021
Merged

VSD - max array length #6293

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
9750b53
Add EXPECT_INDEX & EXPECT_EMPTY_INDEX for more concise array unit tests
jezhiggins Aug 10, 2021
6673edd
Initial unit tests to capture array write behaviour
jezhiggins Aug 10, 2021
c9c80e3
Rework array eval_index to remove out parameter
jezhiggins Aug 12, 2021
5361db1
array insert/replace helper functions
jezhiggins Aug 12, 2021
520a42f
Hardwire maximum array size
jezhiggins Aug 12, 2021
002e1c0
merge writes beyond array maximum length
jezhiggins Aug 12, 2021
627941c
Remove redundant vsd_configt::advanced_sensitivities
jezhiggins Aug 12, 2021
341fae5
Export configuration on object factory, and on abstract_environmentt
jezhiggins Aug 12, 2021
82aa431
Add vsd_configt::maximum_array_index, pick up in full_array_abstract_…
jezhiggins Aug 12, 2021
1426b72
Combined a similiar couple of tests into one with multiple descs
jezhiggins Aug 13, 2021
0a3b7e3
Add --vsd-arrays smash option
jezhiggins Aug 13, 2021
2aafefa
Prevent simultaneous data-dependencies and liveness options
jezhiggins Aug 13, 2021
a78ea94
Bigger array in variable-sensitivity-array-nondet-access tests
jezhiggins Aug 13, 2021
63203b1
Add --vsd-arrays up-to-n-elements option
jezhiggins Aug 13, 2021
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
11 changes: 11 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-access/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
int main(void)
{
int arr[] = {1, 2, 3, 4, 5};
arr[2] = 99;
int arr_0_after_write = arr[0];
int arr_1_after_write = arr[1];
int arr_2_after_write = arr[2];
int arr_3_after_write = arr[3];
int arr_4_after_write = arr[4];
return 0;
}
10 changes: 10 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-access/test-constants-every-element.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values constants --vsd-arrays every-element
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> 1
main::1::arr_1_after_write \(\) -> 2
main::1::arr_2_after_write \(\) -> 99
main::1::arr_3_after_write \(\) -> 4
main::1::arr_4_after_write \(\) -> 5
10 changes: 10 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-access/test-constants-smash.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values constants --vsd-arrays smash
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> TOP
main::1::arr_1_after_write \(\) -> TOP
main::1::arr_2_after_write \(\) -> TOP
main::1::arr_3_after_write \(\) -> TOP
main::1::arr_4_after_write \(\) -> TOP
10 changes: 10 additions & 0 deletions ...sion/goto-analyzer/variable-sensitivity-array-access/test-constants-up-to-3-elements.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> 1
main::1::arr_1_after_write \(\) -> 2
main::1::arr_2_after_write \(\) -> TOP
main::1::arr_3_after_write \(\) -> TOP
main::1::arr_4_after_write \(\) -> TOP
10 changes: 10 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-every-element.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> \[1, 1\]
main::1::arr_1_after_write \(\) -> \[2, 2\]
main::1::arr_2_after_write \(\) -> \[63, 63\]
main::1::arr_3_after_write \(\) -> \[4, 4\]
main::1::arr_4_after_write \(\) -> \[5, 5\]
10 changes: 10 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-smash.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> \[1, 63\]
main::1::arr_1_after_write \(\) -> \[1, 63\]
main::1::arr_2_after_write \(\) -> \[1, 63\]
main::1::arr_3_after_write \(\) -> \[1, 63\]
main::1::arr_4_after_write \(\) -> \[1, 63\]
10 changes: 10 additions & 0 deletions ...sion/goto-analyzer/variable-sensitivity-array-access/test-intervals-up-to-3-elements.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> \[1, 1\]
main::1::arr_1_after_write \(\) -> \[2, 2\]
main::1::arr_2_after_write \(\) -> \[3, 63\]
main::1::arr_3_after_write \(\) -> \[3, 63\]
main::1::arr_4_after_write \(\) -> \[3, 63\]
10 changes: 10 additions & 0 deletions ...ession/goto-analyzer/variable-sensitivity-array-access/test-value-sets-every-element.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end
main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
main::1::arr_2_after_write \(\) -> value-set-begin: 99 :value-set-end
main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end
main::1::arr_4_after_write \(\) -> value-set-begin: 5 :value-set-end
10 changes: 10 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-smash.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
main::1::arr_4_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
10 changes: 10 additions & 0 deletions ...ion/goto-analyzer/variable-sensitivity-array-access/test-value-sets-up-to-3-elements.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
^EXIT=0$
^SIGNAL=0$
main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end
main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
8 changes: 0 additions & 8 deletions regression/goto-analyzer/variable-sensitivity-array-constant-access/main.c
View file
Open in desktop

This file was deleted.

7 changes: 0 additions & 7 deletions regression/goto-analyzer/variable-sensitivity-array-constant-access/test.desc
View file
Open in desktop

This file was deleted.

33 changes: 0 additions & 33 deletions regression/goto-analyzer/variable-sensitivity-array-interval-access/main.c
View file
Open in desktop

This file was deleted.

9 changes: 0 additions & 9 deletions regression/goto-analyzer/variable-sensitivity-array-interval-access/test.desc
View file
Open in desktop

This file was deleted.

13 changes: 7 additions & 6 deletions ...sensitivity-array-value-set-access/main.c → ...le-sensitivity-array-nondet-access/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
int main(void)
{
int arr[] = {1, 2, 3};
int arr[] = {1, 2, 3, 4, 5};
int ix;
if(ix)
{
Expand All @@ -10,24 +10,25 @@ int main(void)
{
ix = 2;
}

// ix is between 0 and 2
// so this is between 1 and 3
int arr_at_ix = arr[ix];

int write_ix;
if(write_ix)
{
write_ix = 0;
}
else
{
write_ix = 1;
write_ix = 4;
}
arr[write_ix] = 4;
arr[write_ix] = 99;
int arr_0_after_write = arr[0];
int arr_1_after_write = arr[1];
// We can't write to arr[2]
// because write_ix is between 0 and 1
// so this should be unchanged
int arr_2_after_write = arr[2];
int arr_3_after_write = arr[3];
int arr_4_after_write = arr[4];
return 0;
}
11 changes: 11 additions & 0 deletions .../goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values constants --vsd-arrays every-element
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> TOP @ \[9\]
main::1::arr_0_after_write \(\) -> TOP @ \[18\]
main::1::arr_1_after_write \(\) -> TOP @ \[20\]
main::1::arr_2_after_write \(\) -> TOP @ \[22\]
main::1::arr_3_after_write \(\) -> TOP @ \[24\]
main::1::arr_4_after_write \(\) -> TOP @ \[26\]
11 changes: 11 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values constants --vsd-arrays smash
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> TOP @ \[9\]
main::1::arr_0_after_write \(\) -> TOP
main::1::arr_1_after_write \(\) -> TOP
main::1::arr_2_after_write \(\) -> TOP
main::1::arr_3_after_write \(\) -> TOP
main::1::arr_4_after_write \(\) -> TOP
11 changes: 11 additions & 0 deletions ...to-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> TOP @ \[9\]
main::1::arr_0_after_write \(\) -> TOP
main::1::arr_1_after_write \(\) -> TOP
main::1::arr_2_after_write \(\) -> TOP
main::1::arr_3_after_write \(\) -> TOP
main::1::arr_4_after_write \(\) -> TOP
11 changes: 11 additions & 0 deletions .../goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\]
main::1::arr_0_after_write \(\) -> \[1, 63\] @ \[18\]
main::1::arr_1_after_write \(\) -> \[2, 63\] @ \[20\]
main::1::arr_2_after_write \(\) -> \[3, 63\] @ \[22\]
main::1::arr_3_after_write \(\) -> \[4, 63\] @ \[24\]
main::1::arr_4_after_write \(\) -> \[5, 63\] @ \[26\]
11 changes: 11 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\]
main::1::arr_0_after_write \(\) -> \[1, 63\]
main::1::arr_1_after_write \(\) -> \[1, 63\]
main::1::arr_2_after_write \(\) -> \[1, 63\]
main::1::arr_3_after_write \(\) -> \[1, 63\]
main::1::arr_4_after_write \(\) -> \[1, 63\]
11 changes: 11 additions & 0 deletions ...to-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\]
main::1::arr_0_after_write \(\) -> \[1, 63\]
main::1::arr_1_after_write \(\) -> \[2, 63\]
main::1::arr_2_after_write \(\) -> \[3, 63\]
main::1::arr_3_after_write \(\) -> \[3, 63\]
main::1::arr_4_after_write \(\) -> \[3, 63\]
11 changes: 11 additions & 0 deletions ...goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-every-element.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> value-set-begin: 1, 3 :value-set-end
main::1::arr_0_after_write \(\) -> value-set-begin: 1, 99 :value-set-end
main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
main::1::arr_2_after_write \(\) -> value-set-begin: 3 :value-set-end
main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end
main::1::arr_4_after_write \(\) -> value-set-begin: 5, 99 :value-set-end
11 changes: 11 additions & 0 deletions regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-smash.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> value-set-begin: 1, 2, 3, 4, 5 :value-set-end
main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
main::1::arr_4_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
11 changes: 11 additions & 0 deletions ...o-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-up-to-3-elements.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
^EXIT=0$
^SIGNAL=0$
main::1::arr_at_ix \(\) -> value-set-begin: 1, 3, 4, 5 :value-set-end
main::1::arr_0_after_write \(\) -> value-set-begin: 1, 99 :value-set-end
main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
9 changes: 0 additions & 9 deletions regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc
View file
Open in desktop

This file was deleted.

5 changes: 2 additions & 3 deletions src/analyses/variable-sensitivity/abstract_environment.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -337,10 +337,9 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory(
type, top, bttm, e, environment, ns);
}

abstract_object_pointert abstract_environmentt::add_object_context(
const abstract_object_pointert &abstract_object) const
const vsd_configt &abstract_environmentt::configuration() const
{
return object_factory->wrap_with_context(abstract_object);
return object_factory->config();
}
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bit of a diff mismatch. add_object_context is redundant and was removed. configuration is a new member function, which we need :)


bool abstract_environmentt::merge(
Expand Down
16 changes: 4 additions & 12 deletions src/analyses/variable-sensitivity/abstract_environment.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,8 @@ enum class widen_modet
could_widen
};

struct vsd_configt;

class abstract_environmentt
{
public:
Expand Down Expand Up @@ -174,18 +176,8 @@ class abstract_environmentt
const exprt &e,
const namespacet &ns) const;

/// Wraps an existing object in any configured context object
///
/// \param abstract_object: The object to be wrapped
///
/// \return The wrapped abstract object
///
/// Look at the configuration context dependency, and constructs
/// the appropriate wrapper object around the supplied object
/// If no such configuration is enabled, the supplied object will be
/// returned unchanged
virtual abstract_object_pointert
add_object_context(const abstract_object_pointert &abstract_object) const;
/// Exposes the environment configuration
const vsd_configt &configuration() const;

/// Computes the join between "this" and "b"
///
Expand Down
Loading