Go to the documentation of this file.
33 :
log(message_handler)
38 const std::string &taint_file_name,
65 for(goto_programt::instructionst::iterator
66 it=goto_function.body.instructions.begin();
67 it!=goto_function.body.instructions.end();
80 if(
function.
id() == ID_symbol)
84 std::set<irep_idt> identifiers;
86 identifiers.insert(identifier);
88 irep_idt class_id =
function.get(ID_C_class);
94 std::string suffix = std::string(
99 for(
const auto &p : parents)
100 identifiers.insert(
id2string(p) + suffix);
106 for(
const auto &i : identifiers)
109 i == rule.function_identifier ||
112 "java::" +
id2string(rule.function_identifier) +
":"))
121 log.
debug() <<
"MATCH " << rule.id <<
" on " << identifier
128 bool have_this = !code_type.
parameters().empty() &&
129 code_type.
parameters().front().get_bool(ID_C_this);
144 have_this ? rule.parameter_number : rule.parameter_number - 1;
145 if(function_call.
arguments().size() > nr)
155 "`this` implies at least one argument in function call");
165 codet code_set_may{ID_set_may};
167 code_set_may.op0() = where;
184 t->source_location.set_property_class(
186 t->source_location.set_comment(rule.message);
192 codet code_clear_may{ID_clear_may};
193 code_clear_may.
operands().resize(2);
194 code_clear_may.op0() = where;
195 code_clear_may.
op1() =
207 if(!insert_before.
empty())
209 goto_function.body.insert_before_swap(it, insert_before);
211 while(!it->is_function_call()) ++it;
214 if(!insert_after.
empty())
216 goto_function.body.destructive_insert(
217 std::next(it), insert_after);
223 const std::string &taint_file_name,
232 bool use_json = json_file_name.has_value();
234 log.
status() <<
"Reading taint file '" << taint_file_name <<
"'"
247 taint.output(mstream);
248 mstream << messaget::eom;
259 bool have_entry_point=
271 <<
"we will consider the heads of all functions as reachable"
279 if(f_it->second.body_available() &&
307 custom_bitvector_analysis(goto_functions, ns);
311 custom_bitvector_analysis.
output(ns, goto_functions, std::cout);
317 if(!f_it->second.body.has_assertion())
322 if(f_it->first==
"__actual_thread_spawn")
329 if(!i_it->is_assert())
333 i_it->get_condition()))
338 if(custom_bitvector_analysis[i_it].has_values.is_false())
342 custom_bitvector_analysis.
eval(i_it->get_condition(), i_it);
351 <<
"******** Function " << symbol.
display_name() <<
'\n';
358 json_stringt(i_it->source_location.get_property_class())},
359 {
"file",
json_stringt(i_it->source_location.get_file())},
366 std::cout << i_it->source_location;
367 if(!i_it->source_location.get_comment().empty())
368 std::cout <<
": " << i_it->source_location.get_comment();
370 if(!i_it->source_location.get_property_class().empty())
372 << i_it->source_location.get_property_class() <<
")";
381 std::ofstream json_out(json_file_name.value());
385 log.
error() <<
"Failed to open json output '" << json_file_name.value()
390 log.
status() <<
"Analysis result is written to '"
393 json_out << json_result <<
'\n';
398 catch(
const char *error_msg)
403 catch(
const std::string &error_msg)
410 log.
error() <<
"Caught unexpected error in taint_analysist::operator()"
418 const std::string &taint_file_name,
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
source_locationt source_location
The location of the instruction in the source file.
Non-graph-based representation of the class hierarchy.
class_hierarchyt class_hierarchy
const irep_idt & display_name() const
Return language specific display name if present.
mstreamt & status() const
void instrument(const namespacet &, goto_functionst &)
Field-insensitive, location-sensitive bitvector analysis.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
bool empty() const
Is the program empty?
Base class for all expressions.
exprt eval(const exprt &src, locationt loc)
function_mapt function_map
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
const irep_idt & get_identifier() const
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
exprt simplify_expr(exprt src, const namespacet &ns)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::vector< irep_idt > idst
bool operator()(const std::string &taint_file_name, const symbol_tablet &, goto_functionst &, bool show_full, const optionalt< std::string > &json_file_name)
bool taint_parser(const std::string &file_name, taint_parse_treet &dest, message_handlert &message_handler)
const parameterst & parameters() const
nonstd::optional< T > optionalt
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
static bool has_get_must_or_may(const exprt &)
message_handlert & get_message_handler()
goto_functionst goto_functions
GOTO functions.
source_locationt location
Source code location of definition of symbol.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const optionalt< std::string > &json_file_name)
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
A generic container class for the GOTO intermediate representation of one function.
symbol_exprt return_value_symbol(const irep_idt &identifier, const namespacet &ns)
produces the symbol that is used to store the return value of the function with the given identifier
#define forall_goto_functions(it, functions)
bool has_prefix(const std::string &s, const std::string &prefix)
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
idst get_parents_trans(const irep_idt &id) const
Operator to return the address of an object.
The Boolean constant true.
bool is_function_call() const
bool is_true(const literalt &l)
taint_analysist(message_handlert &message_handler)
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet symbol_table
Symbol table.
jsont & push_back(const jsont &json)
instructionst::iterator targett
#define forall_goto_program_instructions(it, program)
Data structure for representing an arbitrary statement in a program.