Skip to content

Incremental unwinding of one specified loop #4361

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

Closed
wants to merge 16 commits into from
Closed

Incremental unwinding of one specified loop #4361

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
54d581b
Allow disabling optimized assertion conversion
peterschrammel Feb 9, 2019
452b524
Hidden field is used for hiding in trace
peterschrammel Feb 9, 2019
1fb7d2d
Allow symex to temporarily ignore assertions
peterschrammel Feb 3, 2019
73fb826
Allow symex_target_equationt to separately convert assertions
peterschrammel Feb 3, 2019
41d3864
Use only remaining properties in property decider
peterschrammel Feb 9, 2019
7fbc6b0
Add callback to decide on interrupting goto-symex
peterschrammel Feb 9, 2019
2a7b16c
Add symex BMC incremental one loop
peterschrammel Feb 9, 2019
cef212c
Add single-loop incremental symex checker
peterschrammel Feb 2, 2019
4e894a4
Add options for incremental one-loop BMC
peterschrammel Feb 3, 2019
d7581bd
Add --incremental-loop to CBMC
peterschrammel Feb 3, 2019
30ca986
Fix quoting in test command
peterschrammel Feb 9, 2019
aa1389b
Make sure output buffers are flushed before writing exit code
peterschrammel Mar 10, 2019
657a899
Clean up cbmc-incr-oneloop tests
peterschrammel Feb 9, 2019
cc60ab3
Set induction tests to FUTURE
peterschrammel Feb 10, 2019
f1af977
Clang-format cbmc-incr-oneloop tests
peterschrammel Feb 10, 2019
20613e8
Ignore properties before unwind min
peterschrammel Feb 10, 2019
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: 4 additions & 0 deletions src/goto-symex/goto_symex.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,10 @@ class goto_symext
/// symbolic execution from that state.
bool should_pause_symex;

/// If this flag is set to true then assertions will be temporarily ignored
/// by the symbolic executions.
Copy link
Collaborator

Choose a reason for hiding this comment

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

What exactly does "ignored" mean? Any why is this ever the right thing to do?

bool ignore_assertions = false;

protected:
/// The configuration to use for this symbolic execution
const symex_configt symex_config;
Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/symex_main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -566,7 +566,7 @@ void goto_symext::execute_next_instruction(
break;

case ASSERT:
if(!state.guard.is_false())
if(!state.guard.is_false() && !ignore_assertions)
symex_assert(instruction, state);
symex_transition(state);
break;
Expand Down
9 changes: 5 additions & 4 deletions src/goto-symex/symex_target_equation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -451,7 +451,8 @@ void symex_target_equationt::convert_constraints(
}

void symex_target_equationt::convert_assertions(
decision_proceduret &decision_procedure)
decision_proceduret &decision_procedure,
bool optimized_for_single_assertions)
{
// we find out if there is only _one_ assertion,
// which allows for a simpler formula
Expand All @@ -461,13 +462,13 @@ void symex_target_equationt::convert_assertions(
if(number_of_assertions==0)
return;

if(number_of_assertions==1)
if(number_of_assertions == 1 && optimized_for_single_assertions)
{
for(auto &step : SSA_steps)
{
// ignore already converted assertions in the error trace
if(step.is_assert() && step.converted)
step.ignore = true;
step.hidden = true;
Copy link
Collaborator

Choose a reason for hiding this comment

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

That makes the comment above seem rather odd?


if(step.is_assert() && !step.ignore && !step.converted)
{
Expand All @@ -494,7 +495,7 @@ void symex_target_equationt::convert_assertions(
{
// ignore already converted assertions in the error trace
if(step.is_assert() && step.converted)
step.ignore = true;
step.hidden = true;
Copy link
Collaborator

Choose a reason for hiding this comment

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

As above


if(step.is_assert() && !step.ignore && !step.converted)
{
Expand Down
6 changes: 5 additions & 1 deletion src/goto-symex/symex_target_equation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,11 @@ class symex_target_equationt:public symex_targett

/// Converts assertions: build a disjunction of negated assertions.
/// \param decision_procedure: A handle to a decision procedure interface
void convert_assertions(decision_proceduret &decision_procedure);
/// \param optimized_for_single_assertions: Use an optimized encoding for
/// single assertions (unsound for incremental conversions)
void convert_assertions(
decision_proceduret &decision_procedure,
bool optimized_for_single_assertions = true);

/// Converts constraints: set the represented condition to _True_.
/// \param decision_procedure: A handle to a decision procedure interface
Expand Down