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 1 commit
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
13 changes: 13 additions & 0 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 @@ -321,6 +321,19 @@ void symex_target_equationt::constraint(
merge_ireps(SSA_step);
}

void symex_target_equationt::convert_without_assertions(
decision_proceduret &decision_procedure)
{
convert_guards(decision_procedure);
convert_assignments(decision_procedure);
convert_decls(decision_procedure);
convert_assumptions(decision_procedure);
convert_goto_instructions(decision_procedure);
convert_function_calls(decision_procedure);
convert_io(decision_procedure);
convert_constraints(decision_procedure);
}
Copy link
Collaborator

Choose a reason for hiding this comment

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

Could this be refactored so that we don't have almost-the-same-code twice?


void symex_target_equationt::convert(decision_proceduret &decision_procedure)
{
convert_guards(decision_procedure);
Expand Down
9 changes: 9 additions & 0 deletions src/goto-symex/symex_target_equation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -177,6 +177,15 @@ class symex_target_equationt:public symex_targett
/// \param decision_procedure: A handle to a decision procedure interface
void convert(decision_proceduret &decision_procedure);

/// Interface method to initiate the conversion into a decision procedure
/// format. The method iterates over the equation, i.e. over the SSA steps and
/// converts each type of step separately, except assertions.
/// This enables the caller to handle assertion conversion differently,
/// e.g. for incremental solving.
/// \param decision_procedure: A handle to a particular decision procedure
/// interface
void convert_without_assertions(decision_proceduret &decision_procedure);

/// Converts assignments: set the equality _lhs==rhs_ to _True_.
/// \param decision_procedure: A handle to a decision procedure
/// interface
Expand Down