cprover
taint_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Taint Analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "taint_analysis.h"
13 
14 #include <iostream>
15 #include <fstream>
16 
17 #include <util/invariant.h>
18 #include <util/json.h>
19 #include <util/message.h>
20 #include <util/pointer_expr.h>
21 #include <util/prefix.h>
22 #include <util/simplify_expr.h>
23 #include <util/string_constant.h>
24 
26 
28 
29 #include "taint_parser.h"
30 
32 {
33 public:
34  explicit taint_analysist(message_handlert &message_handler)
35  : log(message_handler)
36  {
37  }
38 
39  bool operator()(
40  const std::string &taint_file_name,
41  const symbol_tablet &,
43  bool show_full,
44  const optionalt<std::string> &json_file_name);
45 
46 protected:
50 
51  void instrument(const namespacet &, goto_functionst &);
53 };
54 
56  const namespacet &ns,
57  goto_functionst &goto_functions)
58 {
59  for(auto &function : goto_functions.function_map)
60  instrument(ns, function.second);
61 }
62 
64  const namespacet &ns,
65  goto_functionst::goto_functiont &goto_function)
66 {
67  for(goto_programt::instructionst::iterator
68  it=goto_function.body.instructions.begin();
69  it!=goto_function.body.instructions.end();
70  it++)
71  {
72  const goto_programt::instructiont &instruction=*it;
73 
74  goto_programt insert_before, insert_after;
75 
76  if(instruction.is_function_call())
77  {
78  const code_function_callt &function_call =
79  instruction.get_function_call();
80  const exprt &function = function_call.function();
81 
82  if(function.id() == ID_symbol)
83  {
84  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
85 
86  std::set<irep_idt> identifiers;
87 
88  identifiers.insert(identifier);
89 
90  irep_idt class_id = function.get(ID_C_class);
91  if(class_id.empty())
92  {
93  }
94  else
95  {
96  std::string suffix = std::string(
97  id2string(identifier), class_id.size(), std::string::npos);
98 
99  class_hierarchyt::idst parents =
101  for(const auto &p : parents)
102  identifiers.insert(id2string(p) + suffix);
103  }
104 
105  for(const auto &rule : taint.rules)
106  {
107  bool match = false;
108  for(const auto &i : identifiers)
109  {
110  if(
111  i == rule.function_identifier ||
112  has_prefix(
113  id2string(i),
114  "java::" + id2string(rule.function_identifier) + ":"))
115  {
116  match = true;
117  break;
118  }
119  }
120 
121  if(match)
122  {
123  log.debug() << "MATCH " << rule.id << " on " << identifier
124  << messaget::eom;
125 
126  exprt where = nil_exprt();
127 
128  const code_typet &code_type = to_code_type(function.type());
129 
130  bool have_this = !code_type.parameters().empty() &&
131  code_type.parameters().front().get_bool(ID_C_this);
132 
133  switch(rule.where)
134  {
136  {
138  ns.lookup(id2string(identifier) + "#return_value");
139  where = return_value_symbol.symbol_expr();
140  break;
141  }
142 
144  {
145  unsigned nr =
146  have_this ? rule.parameter_number : rule.parameter_number - 1;
147  if(function_call.arguments().size() > nr)
148  where = function_call.arguments()[nr];
149  break;
150  }
151 
153  if(have_this)
154  {
156  !function_call.arguments().empty(),
157  "`this` implies at least one argument in function call");
158  where = function_call.arguments()[0];
159  }
160  break;
161  }
162 
163  switch(rule.kind)
164  {
166  {
167  codet code_set_may{ID_set_may};
168  code_set_may.operands().resize(2);
169  code_set_may.op0() = where;
170  code_set_may.op1() =
171  address_of_exprt(string_constantt(rule.taint));
172  insert_after.add(goto_programt::make_other(
173  code_set_may, instruction.source_location));
174  break;
175  }
176 
178  {
179  binary_predicate_exprt get_may{
180  where,
181  ID_get_may,
182  address_of_exprt(string_constantt(rule.taint))};
184  insert_before.add(goto_programt::make_assertion(
185  not_exprt(get_may), instruction.source_location));
186  t->source_location.set_property_class(
187  "taint rule " + id2string(rule.id));
188  t->source_location.set_comment(rule.message);
189  break;
190  }
191 
193  {
194  codet code_clear_may{ID_clear_may};
195  code_clear_may.operands().resize(2);
196  code_clear_may.op0() = where;
197  code_clear_may.op1() =
198  address_of_exprt(string_constantt(rule.taint));
199  insert_after.add(goto_programt::make_other(
200  code_clear_may, instruction.source_location));
201  break;
202  }
203  }
204  }
205  }
206  }
207  }
208 
209  if(!insert_before.empty())
210  {
211  goto_function.body.insert_before_swap(it, insert_before);
212  // advance until we get back to the call
213  while(!it->is_function_call()) ++it;
214  }
215 
216  if(!insert_after.empty())
217  {
218  goto_function.body.destructive_insert(
219  std::next(it), insert_after);
220  }
221  }
222 }
223 
225  const std::string &taint_file_name,
226  const symbol_tablet &symbol_table,
227  goto_functionst &goto_functions,
228  bool show_full,
229  const optionalt<std::string> &json_file_name)
230 {
231  try
232  {
233  json_arrayt json_result;
234  bool use_json = json_file_name.has_value();
235 
236  log.status() << "Reading taint file '" << taint_file_name << "'"
237  << messaget::eom;
238 
239  if(taint_parser(taint_file_name, taint, log.get_message_handler()))
240  {
241  log.error() << "Failed to read taint definition file" << messaget::eom;
242  return true;
243  }
244 
245  log.status() << "Got " << taint.rules.size() << " taint definitions"
246  << messaget::eom;
247 
248  log.conditional_output(log.debug(), [this](messaget::mstreamt &mstream) {
249  taint.output(mstream);
250  mstream << messaget::eom;
251  });
252 
253  log.status() << "Instrumenting taint" << messaget::eom;
254 
255  class_hierarchy(symbol_table);
256 
257  const namespacet ns(symbol_table);
258  instrument(ns, goto_functions);
259  goto_functions.update();
260 
261  bool have_entry_point=
262  goto_functions.function_map.find(goto_functionst::entry_point())!=
263  goto_functions.function_map.end();
264 
265  // do we have an entry point?
266  if(have_entry_point)
267  {
268  log.status() << "Working from entry point" << messaget::eom;
269  }
270  else
271  {
272  log.status() << "No entry point found; "
273  << "we will consider the heads of all functions as reachable"
274  << messaget::eom;
275 
276  goto_programt end, gotos, calls;
277 
279 
280  for(const auto &gf_entry : goto_functions.function_map)
281  {
282  if(
283  gf_entry.second.body_available() &&
284  gf_entry.first != goto_functionst::entry_point())
285  {
286  const symbolt &symbol = ns.lookup(gf_entry.first);
287  const code_function_callt call(symbol.symbol_expr());
290  calls.add(
294  }
295  }
296 
298  goto_functions.function_map[goto_functionst::entry_point()];
299 
300  goto_programt &body=entry.body;
301 
302  body.destructive_append(gotos);
303  body.destructive_append(calls);
304  body.destructive_append(end);
305 
306  goto_functions.update();
307  }
308 
309  log.status() << "Data-flow analysis" << messaget::eom;
310 
311  custom_bitvector_analysist custom_bitvector_analysis;
312  custom_bitvector_analysis(goto_functions, ns);
313 
314  if(show_full)
315  {
316  custom_bitvector_analysis.output(ns, goto_functions, std::cout);
317  return false;
318  }
319 
320  for(const auto &gf_entry : goto_functions.function_map)
321  {
322  if(!gf_entry.second.body.has_assertion())
323  continue;
324 
325  const symbolt &symbol = ns.lookup(gf_entry.first);
326 
327  if(gf_entry.first == "__actual_thread_spawn")
328  continue;
329 
330  bool first=true;
331 
332  forall_goto_program_instructions(i_it, gf_entry.second.body)
333  {
334  if(!i_it->is_assert())
335  continue;
336 
338  i_it->get_condition()))
339  {
340  continue;
341  }
342 
343  if(custom_bitvector_analysis[i_it].has_values.is_false())
344  continue;
345 
346  exprt result =
347  custom_bitvector_analysis.eval(i_it->get_condition(), i_it);
348  if(simplify_expr(std::move(result), ns).is_true())
349  continue;
350 
351  if(first)
352  {
353  first=false;
354  if(!use_json)
355  std::cout << "\n"
356  << "******** Function " << symbol.display_name() << '\n';
357  }
358 
359  if(use_json)
360  {
362  {"bugClass",
363  json_stringt(i_it->source_location.get_property_class())},
364  {"file", json_stringt(i_it->source_location.get_file())},
365  {"line",
366  json_numbert(id2string(i_it->source_location.get_line()))}};
367  json_result.push_back(std::move(json));
368  }
369  else
370  {
371  std::cout << i_it->source_location;
372  if(!i_it->source_location.get_comment().empty())
373  std::cout << ": " << i_it->source_location.get_comment();
374 
375  if(!i_it->source_location.get_property_class().empty())
376  std::cout << " ("
377  << i_it->source_location.get_property_class() << ")";
378 
379  std::cout << '\n';
380  }
381  }
382  }
383 
384  if(use_json)
385  {
386  std::ofstream json_out(json_file_name.value());
387 
388  if(!json_out)
389  {
390  log.error() << "Failed to open json output '" << json_file_name.value()
391  << "'" << messaget::eom;
392  return true;
393  }
394 
395  log.status() << "Analysis result is written to '"
396  << json_file_name.value() << "'" << messaget::eom;
397 
398  json_out << json_result << '\n';
399  }
400 
401  return false;
402  }
403  catch(const char *error_msg)
404  {
405  log.error() << error_msg << messaget::eom;
406  return true;
407  }
408  catch(const std::string &error_msg)
409  {
410  log.error() << error_msg << messaget::eom;
411  return true;
412  }
413  catch(...)
414  {
415  log.error() << "Caught unexpected error in taint_analysist::operator()"
416  << messaget::eom;
417  return true;
418  }
419 }
420 
422  goto_modelt &goto_model,
423  const std::string &taint_file_name,
424  message_handlert &message_handler,
425  bool show_full,
426  const optionalt<std::string> &json_file_name)
427 {
428  taint_analysist taint_analysis(message_handler);
429  return taint_analysis(
430  taint_file_name,
431  goto_model.symbol_table,
432  goto_model.goto_functions,
433  show_full,
434  json_file_name);
435 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
json_numbert
Definition: json.h:291
taint_parse_treet::rules
rulest rules
Definition: taint_parser.h:63
taint_analysist::log
messaget log
Definition: taint_analysis.cpp:47
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:431
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
taint_analysist::class_hierarchy
class_hierarchyt class_hierarchy
Definition: taint_analysis.cpp:49
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
messaget::status
mstreamt & status() const
Definition: message.h:414
taint_analysist::instrument
void instrument(const namespacet &, goto_functionst &)
Definition: taint_analysis.cpp:55
custom_bitvector_analysis.h
Field-insensitive, location-sensitive bitvector analysis.
taint_parser.h
Taint Parser.
taint_parse_treet
Definition: taint_parser.h:24
taint_analysist
Definition: taint_analysis.cpp:32
prefix.h
taint_analysis.h
Taint Analysis.
invariant.h
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1015
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
string_constant.h
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:826
taint_parse_treet::rulet::RETURN_VALUE
@ RETURN_VALUE
Definition: taint_parser.h:30
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
custom_bitvector_analysist::eval
exprt eval(const exprt &src, locationt loc)
Definition: custom_bitvector_analysis.h:156
bool_typet
The Boolean type.
Definition: std_types.h:36
messaget::eom
static eomt eom
Definition: message.h:297
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
string_constantt
Definition: string_constant.h:15
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1056
taint_analysist::taint
taint_parse_treet taint
Definition: taint_analysis.cpp:48
json_arrayt
Definition: json.h:165
json_objectt
Definition: json.h:300
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1107
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
messaget::error
mstreamt & error() const
Definition: message.h:399
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
taint_parse_treet::rulet::THIS
@ THIS
Definition: taint_parser.h:30
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:116
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
goto_programt::instructiont::get_function_call
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:353
exprt::op1
exprt & op1()
Definition: expr.h:102
taint_parse_treet::rulet::SANITIZER
@ SANITIZER
Definition: taint_parser.h:29
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2659
custom_bitvector_analysist
Definition: custom_bitvector_analysis.h:149
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
code_typet
Base type of functions.
Definition: std_types.h:539
message_handlert
Definition: message.h:28
class_hierarchyt::idst
std::vector< irep_idt > idst
Definition: class_hierarchy.h:45
taint_analysist::operator()
bool operator()(const std::string &taint_file_name, const symbol_tablet &, goto_functionst &, bool show_full, const optionalt< std::string > &json_file_name)
Definition: taint_analysis.cpp:224
taint_parser
bool taint_parser(const std::string &file_name, taint_parse_treet &dest, message_handlert &message_handler)
Definition: taint_parser.cpp:20
dstringt::empty
bool empty() const
Definition: dstring.h:88
taint_parse_treet::rulet::PARAMETER
@ PARAMETER
Definition: taint_parser.h:30
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1258
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
simplify_expr.h
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
custom_bitvector_domaint::has_get_must_or_may
static bool has_get_must_or_may(const exprt &)
Definition: custom_bitvector_analysis.cpp:685
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
class_hierarchy.h
Class Hierarchy.
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
ai_baset::output
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.
Definition: ai.cpp:40
symbolt
Symbol table entry.
Definition: symbol.h:28
taint_analysis
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)
Definition: taint_analysis.cpp:421
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
messaget::conditional_output
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...
Definition: message.cpp:139
goto_functionst::update
void update()
Definition: goto_functions.h:83
json.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
taint_parse_treet::rulet::SOURCE
@ SOURCE
Definition: taint_parser.h:29
return_value_symbol
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
Definition: remove_returns.cpp:406
messaget::mstreamt
Definition: message.h:224
exprt::operands
operandst & operands()
Definition: expr.h:92
messaget::debug
mstreamt & debug() const
Definition: message.h:429
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
class_hierarchyt::get_parents_trans
idst get_parents_trans(const irep_idt &id) const
Definition: class_hierarchy.h:76
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
taint_parse_treet::rulet::SINK
@ SINK
Definition: taint_parser.h:29
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:530
is_true
bool is_true(const literalt &l)
Definition: literal.h:198
taint_analysist::taint_analysist
taint_analysist(message_handlert &message_handler)
Definition: taint_analysis.cpp:34
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
code_function_callt::function
exprt & function()
Definition: std_code.h:1248
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1255
dstringt::size
size_t size() const
Definition: dstring.h:104
json_stringt
Definition: json.h:270
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
not_exprt
Boolean negation.
Definition: std_expr.h:2127