37 const std::string &taint_file_name,
41 const std::string &json_file_name);
63 for(goto_programt::instructionst::iterator
64 it=goto_function.body.instructions.begin();
65 it!=goto_function.body.instructions.end();
72 switch(instruction.
type)
80 if(
function.
id()==ID_symbol)
85 std::set<irep_idt> identifiers;
87 identifiers.insert(identifier);
89 irep_idt class_id=
function.get(ID_C_class);
101 for(
const auto &p : parents)
108 for(
const auto &i : identifiers)
109 if(i==rule.function_identifier ||
112 "java::"+
id2string(rule.function_identifier)+
":"))
120 debug() <<
"MATCH " << rule.id <<
" on " << identifier <<
eom;
128 code_type.
parameters().front().get_bool(ID_C_this);
134 const symbolt &return_value_symbol=
143 have_this?rule.parameter_number:rule.parameter_number-1;
154 "`this` implies at least one argument in function call");
164 codet code_set_may(
"set_may");
166 code_set_may.
op0()=where;
170 t->make_other(code_set_may);
185 t->source_location.set_comment(rule.message);
191 codet code_clear_may(
"clear_may");
192 code_clear_may.
operands().resize(2);
193 code_clear_may.
op0()=where;
194 code_clear_may.
op1()=
197 t->make_other(code_clear_may);
213 if(!insert_before.
empty())
215 goto_function.body.insert_before_swap(it, insert_before);
217 while(!it->is_function_call()) ++it;
220 if(!insert_after.
empty())
222 goto_function.body.destructive_insert(
223 std::next(it), insert_after);
229 const std::string &taint_file_name,
233 const std::string &json_file_name)
238 bool use_json=!json_file_name.empty();
240 status() <<
"Reading taint file `" << taint_file_name
245 error() <<
"Failed to read taint definition file" <<
eom;
250 <<
" taint definitions" <<
eom;
255 status() <<
"Instrumenting taint" <<
eom;
263 bool have_entry_point=
270 status() <<
"Working from entry point" <<
eom;
274 status() <<
"No entry point found; " 275 <<
"we will consider the heads of all functions as reachable" 283 if(f_it->second.body_available() &&
288 t->make_function_call(call);
309 custom_bitvector_analysis(goto_functions, ns);
313 custom_bitvector_analysis.
output(ns, goto_functions, std::cout);
319 if(!f_it->second.body.has_assertion())
324 if(f_it->first==
"__actual_thread_spawn")
331 if(!i_it->is_assert())
336 if(custom_bitvector_analysis[i_it].has_values.is_false())
350 <<
"******** Function " << symbol.
display_name() <<
'\n';
357 json_stringt(i_it->source_location.get_property_class());
365 std::cout << i_it->source_location;
366 if(!i_it->source_location.get_comment().empty())
367 std::cout <<
": " << i_it->source_location.get_comment();
369 if(!i_it->source_location.get_property_class().empty())
371 << i_it->source_location.get_property_class() <<
")";
380 std::ofstream json_out(json_file_name);
384 error() <<
"Failed to open json output `" 385 << json_file_name <<
"'" <<
eom;
389 status() <<
"Analysis result is written to `" 390 << json_file_name <<
"'" <<
eom;
392 json_out << json_result <<
'\n';
397 catch(
const char *error_msg)
402 catch(
const std::string &error_msg)
409 error() <<
"Caught unexpected error in taint_analysist::operator()" <<
eom;
416 const std::string &taint_file_name,
419 const std::string &json_file_name)
Field-insensitive, location-sensitive bitvector analysis.
const std::string & id2string(const irep_idt &d)
void set_property_class(const irep_idt &property_class)
Non-graph-based representation of the class hierarchy.
exprt simplify_expr(const exprt &src, const namespacet &ns)
goto_program_instruction_typet type
What kind of instruction?
void output(std::ostream &) const
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const irep_idt & get_identifier() const
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
bool is_true() const
Return whether the expression is a constant representing true.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
bool taint_analysis(goto_modelt &goto_model, const std::string &taint_file_name, message_handlert &message_handler, bool show_full, const std::string &json_file_name)
class_hierarchyt class_hierarchy
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void instrument(const namespacet &, goto_functionst &)
instructionst::iterator targett
instructionst instructions
The list of instructions in the goto program.
static bool has_get_must_or_may(const exprt &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
A side_effect_exprt that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
codet representation of a function call statement.
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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.
Operator to return the address of an object.
std::vector< irep_idt > idst
A generic container class for the GOTO intermediate representation of one function.
const irep_idt & display_name() const
Return language specific display name if present.
bool taint_parser(const std::string &file_name, taint_parse_treet &dest, message_handlert &message_handler)
message_handlert & get_message_handler()
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
mstreamt & result() const
mstreamt & status() const
source_locationt source_location
The location of the instruction in the source file.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
const parameterst & parameters() const
bool empty() const
Is the program empty?
bool operator()(const std::string &taint_file_name, const symbol_tablet &, goto_functionst &, bool show_full, const std::string &json_file_name)
exprt eval(const exprt &src, locationt loc)
Data structure for representing an arbitrary statement in a program.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
idst get_parents_trans(const irep_idt &id) const
goto_functionst goto_functions
GOTO functions.
json_objectt json(const source_locationt &location)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const code_function_callt & to_code_function_call(const codet &code)