Skip to content

Preparation to make goto-analyzer work with the goto_verifiert framework #4703

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 2 commits into from
Jun 3, 2019
Merged

Preparation to make goto-analyzer work with the goto_verifiert framework #4703

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c1b3ffb
Make ai_baset::operator() work with abstract_goto_modelt
hannes-steffenhagen-diffblue May 24, 2019
0f4a362
Add a version of static_verifier that works with propertiest
hannes-steffenhagen-diffblue May 24, 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
12 changes: 6 additions & 6 deletions src/analyses/ai.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,12 +68,12 @@ class ai_baset
}

/// Run abstract interpretation on a whole program
void operator()(const goto_modelt &goto_model)
void operator()(const abstract_goto_modelt &goto_model)
{
const namespacet ns(goto_model.symbol_table);
initialize(goto_model.goto_functions);
entry_state(goto_model.goto_functions);
fixedpoint(goto_model.goto_functions, ns);
const namespacet ns(goto_model.get_symbol_table());
initialize(goto_model.get_goto_functions());
entry_state(goto_model.get_goto_functions());
fixedpoint(goto_model.get_goto_functions(), ns);
finalize();
}

Expand Down Expand Up @@ -374,7 +374,7 @@ class ai_baset
/// \ref ai_baset#operator()(const irep_idt&,const goto_programt&, <!--
/// --> const namespacet&),
/// \ref ai_baset#operator()(const goto_functionst&,const namespacet&)
/// and \ref ai_baset#operator()(const goto_modelt&)
/// and \ref ai_baset#operator()(const abstract_goto_modelt&)
/// 2. Accessing the results of an analysis, by looking up the result
/// for a given location \p l using
/// \ref ait#operator[](goto_programt::const_targett).
Expand Down
1 change: 1 addition & 0 deletions src/goto-analyzer/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ target_link_libraries(goto-analyzer-lib
cpp
linking
big-int
goto-checker
goto-programs
analyses
pointer-analysis
Expand Down
1 change: 1 addition & 0 deletions src/goto-analyzer/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
../cpp/cpp$(LIBEXT) \
../linking/linking$(LIBEXT) \
../big-int/big-int$(LIBEXT) \
../goto-checker/goto-checker$(LIBEXT) \
../goto-programs/goto-programs$(LIBEXT) \
../analyses/analyses$(LIBEXT) \
../pointer-analysis/pointer-analysis$(LIBEXT) \
Expand Down
1 change: 1 addition & 0 deletions src/goto-analyzer/module_dependencies.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ analyses
assembler
cpp
goto-analyzer
goto-checker
goto-programs
java_bytecode # will go away
langapi # should go away
Expand Down
43 changes: 43 additions & 0 deletions src/goto-analyzer/static_verifier.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,49 @@ struct static_verifier_resultt
irep_idt function_id;
};

void static_verifier(
const abstract_goto_modelt &abstract_goto_model,
const ai_baset &ai,
propertiest &properties)
{
const namespacet ns{abstract_goto_model.get_symbol_table()};
// this is mutable because we want to change the property status
// in this loop
for(auto &property : properties)
{
auto &property_status = property.second.status;
const goto_programt::const_targett &property_location = property.second.pc;
exprt condition = property_location->get_condition();
const std::unique_ptr<ai_baset::statet> predecessor_state_copy =
ai.abstract_state_before(property_location);
// simplify the condition given the domain information we have
// about the state right before the assertion is evaluated
predecessor_state_copy->ai_simplify(condition, ns);
// if the condition simplifies to true the assertion always succeeds
if(condition.is_true())
{
property_status = property_statust::PASS;
}
// if the condition simplifies to false the assertion always fails
else if(condition.is_false())
{
property_status = property_statust::FAIL;
Copy link
Member

Choose a reason for hiding this comment

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

Is this a definite fail? If not, then it should be UNKNOWN.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, if a condition is false that means that using domain information it could be simplified to false, i.e. definite fail.

}
// if the domain state is bottom then the assertion is definitely
// unreachable
else if(predecessor_state_copy->is_bottom())
{
property_status = property_statust::NOT_REACHABLE;
}
// if the condition isn't definitely true, false or unreachable
// we don't know whether or not it may fail
else
{
property_status = property_statust::UNKNOWN;
Copy link
Member

Choose a reason for hiding this comment

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

How can this happen? If the location is never assigned a value then it should be NOT_REACHED.

Copy link
Contributor Author

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue May 28, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

This means the condition could not be simplified to true or false using domain information (so it's neither definite fail or success) and the domain state at the location is not bottom so the location is reachable (edit: or rather, potentially reachable), therefore it is unknown.

Copy link
Contributor

Choose a reason for hiding this comment

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

It would be helpful to have this commentary on the various states in the code as well, and not just in the PR :-)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I added some comments explaining what was going on

}
}
}

/// Makes a status message string from a status.
static const char *message(const static_verifier_resultt::statust &status)
{
Expand Down
13 changes: 13 additions & 0 deletions src/goto-analyzer/static_verifier.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
#ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
#define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H

#include <goto-checker/properties.h>
#include <iosfwd>

class abstract_goto_modelt;
class ai_baset;
class goto_modelt;
class message_handlert;
Expand All @@ -23,4 +25,15 @@ bool static_verifier(
message_handlert &,
std::ostream &);

/// Use the information from the abstract interpreter to fill out the statuses
/// of the passed properties
/// \param abstract_goto_model The goto program to verify
/// \param ai The abstract interpreter (should be run to fixpoint
/// before calling this function)
/// \param properties The properties to fill out
void static_verifier(
Copy link
Contributor

Choose a reason for hiding this comment

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

This should be documented. And it's a bit confusing to use a noun for a function which is returning void. (for me "verifier" here should imply you return an object which has a verify method)

Copy link
Contributor Author

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue May 29, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

This is doing more or less the same thing as the other static_verifier function that already is in this file, the only difference is that it writes the result to the propertiest passed in rather than writing them to stdout or to a file.

The "return" value here is the properties parameter (it's an in/out parameter, we read some information from each property and write its verification status back to it)

const abstract_goto_modelt &abstract_goto_model,
const ai_baset &ai,
propertiest &properties);

#endif // CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H