Skip to content

Improvements to goto-analyzer's constant propagator and simplifier [blocks: #2522] #2132

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 10 commits into from
Dec 19, 2018
Merged

Improvements to goto-analyzer's constant propagator and simplifier [blocks: #2522] #2132

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
64b6a6a
Mark tests using --variable as FUTURE
tautschnig Nov 7, 2018
edcf7b8
Update test results and mark tests as passing
tautschnig Nov 7, 2018
fe8d1db
Constant propagation: genuinely use the argument passed to assign_rec
tautschnig Nov 10, 2018
87794c5
Re-enable two-way constant propagation
tautschnig Nov 14, 2018
9e4425a
address-of-dereference may also permit constant propagation
tautschnig May 22, 2018
c23e8ee
Use central is_constantt to identify constants for propagation
tautschnig Apr 27, 2018
2249288
Use extended interpretation of "is constant"
tautschnig Apr 27, 2018
11f92da
Expression rewriting may enable further constant propagation
tautschnig Apr 27, 2018
e367dbc
Constant propagation: Support non-symbol left-hand sides, soundness
tautschnig Nov 14, 2018
2359689
Use constant propagation to dereference left-hand sides
tautschnig Nov 14, 2018
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
4 changes: 2 additions & 2 deletions regression/goto-analyzer/constant_propagation_03/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
FUTURE
CORE
main.c
--constants --simplify out.gb
^EXIT=0$
^SIGNAL=0$
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
--
^warning: ignoring
4 changes: 2 additions & 2 deletions regression/goto-analyzer/constant_propagation_04/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
FUTURE
CORE
main.c
--constants --simplify out.gb
^EXIT=0$
^SIGNAL=0$
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
--
^warning: ignoring
4 changes: 2 additions & 2 deletions regression/goto-analyzer/constant_propagation_05/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
FUTURE
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] file main.c line 12 function main, assertion j != 3: FAILURE \(if reachable\)$
^\[main.assertion.1\] line 11 assertion j != 3: FAILURE \(if reachable\)$
--
^warning: ignoring
6 changes: 3 additions & 3 deletions regression/goto-analyzer/constant_propagation_07/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
FUTURE
CORE
main.c
--constants --simplify out.gb
^EXIT=0$
^SIGNAL=0$
^Simplified: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 11, function calls: 0$
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
--
^warning: ignoring
7 changes: 3 additions & 4 deletions regression/goto-analyzer/constant_propagation_09/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,8 @@
FUTURE
CORE
main.c
--constants --simplify out.gb
--constants --verify
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why has this changed task?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

For completeness: I have changed the task here as simplification did always take place, but not enough of it to actually turn the assertion into a firm FALSE.

^EXIT=0$
^SIGNAL=0$
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 0: FAILURE \(if reachable\)$
--
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'm not sure this change matches the commit message of the commit it is in but I guess it is being updated elsewhere in the patch set, in which case it's a bit unnecessary to change it.

^warning: ignoring
4 changes: 2 additions & 2 deletions regression/goto-analyzer/constant_propagation_10/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
FUTURE
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] file main.c line 10 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE$
^\[main.assertion.1\] line 10 assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE \(if reachable\)$
--
^warning: ignoring
7 changes: 3 additions & 4 deletions regression/goto-analyzer/constant_propagation_11/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,8 @@
FUTURE
CORE
main.c
--constants --simplify out.gb
--constants --verify
Copy link
Collaborator

Choose a reason for hiding this comment

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

Again, why change task?

^EXIT=0$
^SIGNAL=0$
^Simplified: assert: 1, assume: 0, goto: 0, assigns: 0, function calls: 0$
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 0, function calls: 0$
^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 1: SUCCESS$
--
^warning: ignoring
6 changes: 3 additions & 3 deletions regression/goto-analyzer/constant_propagation_12/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
FUTURE
CORE
main.c
--constants --simplify out.gb
^EXIT=0$
^SIGNAL=0$
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$
^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
--
^warning: ignoring
4 changes: 2 additions & 2 deletions regression/goto-analyzer/constant_propagation_13/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
FUTURE
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] file main.c line 9 function main, assertion y == 0: FAILURE \(if reachable\)$
^\[main.assertion.1\] line 9 assertion y == 0: FAILURE \(if reachable\)$
--
^warning: ignoring
6 changes: 3 additions & 3 deletions regression/goto-analyzer/constant_propagation_14/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
FUTURE
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] file main.c line 11 function main, assertion tmp_if_expr: SUCCESS$
^\[main.assertion.2\] file main.c line 12 function main, assertion tmp_if_expr\$1: FAILURE$
^\[main.assertion.1\] line 11 assertion tmp_if_expr: SUCCESS$
^\[main.assertion.2\] line 12 assertion tmp_if_expr\$0: FAILURE \(if reachable\)$
--
^warning: ignoring
4 changes: 2 additions & 2 deletions regression/goto-analyzer/constant_propagation_15/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
FUTURE
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] file main.c line 9 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE$
^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE \(if reachable\)$
--
^warning: ignoring
8 changes: 8 additions & 0 deletions regression/goto-analyzer/constant_propagation_18/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#include <assert.h>

int main()
{
int i = 1;
int *p = &i;
assert(*p == 1);
}
8 changes: 8 additions & 0 deletions regression/goto-analyzer/constant_propagation_18/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] line 7 assertion \*p == 1: SUCCESS$
--
^warning: ignoring
10 changes: 10 additions & 0 deletions regression/goto-analyzer/constant_propagation_19/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
#include <assert.h>

int main()
{
int x;
int *p = &x;
*p = 42;
assert(x == 42);
return 0;
}
8 changes: 8 additions & 0 deletions regression/goto-analyzer/constant_propagation_19/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
Copy link
Contributor

Choose a reason for hiding this comment

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

Would it be possible to call this new test something a little more descriptive, such as constant_propagation_two_way_1 or something?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Done.

main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] line 8 assertion x == 42: SUCCESS$
--
^warning: ignoring
11 changes: 11 additions & 0 deletions regression/goto-analyzer/constant_propagation_two_way_1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
#include <assert.h>

int main()
{
int x;
if(x == 0)
{
assert(!x);
}
return 0;
}
8 changes: 8 additions & 0 deletions regression/goto-analyzer/constant_propagation_two_way_1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
main.c
--constants --verify
^EXIT=0$
^SIGNAL=0$
^\[main.assertion.1\] line 8 assertion !x: SUCCESS$
--
^warning: ignoring
2 changes: 1 addition & 1 deletion regression/goto-analyzer/sensitivity-function-call-recursive/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
FUTURE
main.c
--variable --pointers --arrays --structs --verify
Copy link
Collaborator

Choose a reason for hiding this comment

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

These should be future, also, the names for options should change.

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
FUTURE
sensitivity_test_constants_pointer_to_constants_struct.c
--variable --pointers --structs --verify
^EXIT=0$
Expand Down
Loading