Skip to content

Assume relation between two symbols #5362

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.

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 2 commits into from
Jun 5, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
15 changes: 15 additions & 0 deletions regression/goto-analyzer/intervals_simple-loops/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
#include <assert.h>
const int g_N = 2;

void main(void)
{
for(int i = 0; i < g_N; i++)
{
assert(0);
}

for(int j = 4; j >= g_N; j--)
{
assert(0);
}
}
11 changes: 11 additions & 0 deletions regression/goto-analyzer/intervals_simple-loops/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--intervals
^EXIT=0$
^SIGNAL=0$
\[main\.assertion\.1\] line 8 assertion 0: UNKNOWN
\[main\.assertion\.2\] line 13 assertion 0: UNKNOWN
--
--
Test comparision between two symbols does not mark the
Copy link
Contributor

Choose a reason for hiding this comment

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

This is a do-not-match line, not a comment

result as bottom
8 changes: 4 additions & 4 deletions src/analyses/interval_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -329,10 +329,10 @@ void interval_domaint::assume_rec(
{
integer_intervalt &lhs_i=int_map[lhs_identifier];
integer_intervalt &rhs_i=int_map[rhs_identifier];
lhs_i.meet(rhs_i);
rhs_i=lhs_i;
if(rhs_i.is_bottom())
make_bottom();
if(id == ID_lt && !lhs_i.is_less_than(rhs_i))
lhs_i.make_less_than(rhs_i);
if(id == ID_le && !lhs_i.is_less_than_eq(rhs_i))
lhs_i.make_less_than_eq(rhs_i);
}
else if(is_float(lhs.type()) && is_float(rhs.type()))
{
Expand Down
41 changes: 41 additions & 0 deletions src/util/interval_template.h
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,47 @@ template<class T> class interval_templatet
}
}

void make_bottom()
{
lower_set = upper_set = true;
upper = T();
lower = upper + 1;
}

void make_less_than_eq(interval_templatet &i)
{
if(upper_set && i.upper_set)
Copy link
Contributor

Choose a reason for hiding this comment

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

If my own upper bound is not set but i's is, shouldn't it now become set, and the same for i's lower bound inheriting mine?

upper = std::min(upper, i.upper);
if(lower_set && i.lower_set)
i.lower = std::max(lower, i.lower);
}

void make_less_than(interval_templatet &i)
{
make_less_than_eq(i);
if(singleton() && i.singleton() && lower == i.lower)
Copy link
Contributor

Choose a reason for hiding this comment

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

Shouldn't this do more, too? For example, if i has max 5 and this is now always less than it, this should have max value 4, and similarly i's lower bound should be max(i.lower, lower + 1)?

Choose a reason for hiding this comment

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

@smowton It can do a lot more, but the nice thing about AI is that as long as we don’t add impossible behaviour we don’t necessarily have to do everything as precise as possible from the start (we should make it as precise as reasonable obviously, and there’s a lot of things that still could be done here).

{
make_bottom();
i.make_bottom();
}
}

bool is_less_than_eq(const interval_templatet &i)
{
if(i.lower_set && upper_set && upper <= i.lower)
Copy link
Contributor

Choose a reason for hiding this comment

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

if(x) return true; else return false; --> return x

Copy link
Contributor

Choose a reason for hiding this comment

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

Cross-check since there are no comments to this effect in interval_template.h: these intervals are inclusive at both ends?

return true;
else
return false;
}

bool is_less_than(const interval_templatet &i)
{
if(i.lower_set && upper_set && upper < i.lower)
return true;
else
return false;
}

void approx_union_with(const interval_templatet &i)
{
if(i.lower_set && lower_set)
Expand Down