cprover
model_argc_argv.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Initialize command line arguments
4 
5 Author: Michael Tautschnig
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "model_argc_argv.h"
15 
16 #include <sstream>
17 
18 #include <util/cprover_prefix.h>
19 #include <util/invariant.h>
20 #include <util/message.h>
21 #include <util/namespace.h>
22 #include <util/config.h>
23 #include <util/replace_symbol.h>
24 #include <util/symbol_table.h>
25 #include <util/prefix.h>
26 
27 #include <ansi-c/ansi_c_language.h>
28 
32 
33 // Escape selected character in specified string with backslashes.
34 //
35 // \param input_string: string where character will be escaped.
36 // \param find_substring: character to escape, e.g. \"
37 // \param replace_substring: string, e.g. \\\"
38 std::string escape_char(
39  std::string input_string,
40  std::string find_substring,
41  std::string replace_substring){
42  size_t index = 0;
43  while (true) {
44  /* Locate the substring to replace. */
45  index = input_string.find(find_substring, index);
46 
47  if (index == std::string::npos) break;
48 
49  /* Make the replacement. */
50  input_string.replace(index,
51  replace_substring.size(),
52  replace_substring);
53 
54  /* Advance index forward so the next iteration
55  * doesn't pick it up as well. */
56  index += replace_substring.size();
57  }
58  return input_string;
59 }
60 
75  goto_modelt &goto_model,
76  const std::list<std::string> &argv_args,
77  bool model_argv,
78  message_handlert &message_handler)
79 {
80  messaget message(message_handler);
81  const namespacet ns(goto_model.symbol_table);
82 
83  if(!goto_model.symbol_table.has_symbol(
84  goto_model.goto_functions.entry_point()))
85  {
86  message.error() << "Linking not done, missing "
87  << goto_model.goto_functions.entry_point()
88  << messaget::eom;
89  return true;
90  }
91 
92  const symbolt &main_symbol =
93  ns.lookup(config.main.has_value() ? config.main.value() : ID_main);
94 
95  if(main_symbol.mode!=ID_C)
96  {
97  message.error() << "argc/argv modelling is C specific"
98  << messaget::eom;
99  return true;
100  }
101 
102  const code_typet::parameterst &parameters=
103  to_code_type(main_symbol.type).parameters();
104  if(parameters.size()!=2 &&
105  parameters.size()!=3)
106  {
107  message.warning() << "main expected to take 2 or 3 arguments,"
108  << " argc/argv instrumentation skipped"
109  << messaget::eom;
110  return false;
111  }
112 
113  const symbolt &argc_primed = ns.lookup("argc'");
114  symbol_exprt ARGC("ARGC", argc_primed.type);
115  const symbolt &argv_primed = ns.lookup("argv'");
116  symbol_exprt ARGV("ARGV", argv_primed.type);
117 
118  // set the size of ARGV storage to 4096, which matches the minimum
119  // guaranteed by POSIX (_POSIX_ARG_MAX):
120  // http://pubs.opengroup.org/onlinepubs/009695399/basedefs/limits.h.html
121  std::ostringstream oss;
122  unsigned max_argc = argv_args.size();
123  unsigned argc = argv_args.size();
124 
125  if(model_argv)
126  {
127  oss << "int ARGC;\n"
128  << "char *ARGV[1];\n"
129  << "void " << goto_model.goto_functions.entry_point() << "()\n"
130  << "{\n"
131  << " unsigned next=0u;\n"
132  << " " CPROVER_PREFIX "assume(ARGC>=1);\n"
133  << " " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
134  << " char arg_string[4096];\n"
135  << " " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n"
136  << " for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
137  << " {\n"
138  << " unsigned len;\n"
139  << " " CPROVER_PREFIX "assume(len<4096);\n"
140  << " " CPROVER_PREFIX "assume(next+len<4096);\n"
141  << " " CPROVER_PREFIX "assume(arg_string[next+len]==0);\n"
142  << " ARGV[i]=&(arg_string[next]);\n"
143  << " next+=len+1;\n"
144  << " }\n"
145  << "}";
146  }
147  else
148  { // model_argv = false, set each argv[i] explicitly
149  oss << "int ARGC = " << argc << ";\n"
150  << "char *ARGV[" << argc << "];\n"
151  << "void " << goto_model.goto_functions.entry_point() << "()\n"
152  << "{\n"
153  << "int ARGC = " << argc << ";\n";
154  int i = 0;
155  for(auto &arg : argv_args)
156  {
157  oss << "ARGV[" << i << "]=\"" << escape_char(
158  escape_char(
159  escape_char(arg, "\\","\\\\"),
160  "\'","\\\'"),
161  "\"","\\\"")
162  << "\";\n";
163  i++;
164  }
165  oss << "}";
166  }
167 
168  std::istringstream iss(oss.str());
169 
170  ansi_c_languaget ansi_c_language;
171  ansi_c_language.set_message_handler(message_handler);
174  ansi_c_language.parse(iss, "");
176 
177  symbol_tablet tmp_symbol_table;
178  ansi_c_language.typecheck(tmp_symbol_table, "<built-in-library>");
179 
180  goto_programt init_instructions;
181  exprt value=nil_exprt();
182  // locate the body of the newly built start function as well as any
183  // additional declarations we might need; the body will then be
184  // converted and inserted into the start function
185  for(const auto &symbol_pair : tmp_symbol_table.symbols)
186  {
187  // add __CPROVER_assume if necessary (it might exist already)
188  if(
189  symbol_pair.first == CPROVER_PREFIX "assume" ||
190  symbol_pair.first == CPROVER_PREFIX "input")
191  goto_model.symbol_table.add(symbol_pair.second);
192  else if(symbol_pair.first == goto_model.goto_functions.entry_point())
193  {
194  value = symbol_pair.second.value;
195 
197  replace.insert(ARGC, ns.lookup("argc'").symbol_expr());
198  replace.insert(ARGV, ns.lookup("argv'").symbol_expr());
199  replace(value);
200  }
201  else if(
202  has_prefix(
203  id2string(symbol_pair.first),
204  id2string(goto_model.goto_functions.entry_point()) + "::") &&
205  goto_model.symbol_table.add(symbol_pair.second))
206  UNREACHABLE;
207  }
208  POSTCONDITION(value.is_not_nil());
209 
210  goto_convert(
211  to_code(value),
212  goto_model.symbol_table,
213  init_instructions,
214  message_handler,
215  main_symbol.mode);
216 
217  for(auto &instruction : init_instructions.instructions)
218  instruction.source_location_nonconst().set_file("<built-in-library>");
219 
220  goto_functionst::function_mapt::iterator start_entry=
221  goto_model.goto_functions.function_map.find(
222  goto_model.goto_functions.entry_point());
223 
225  start_entry!=goto_model.goto_functions.function_map.end() &&
226  start_entry->second.body_available(),
227  "entry point expected to have a body");
228 
229  goto_programt &start=start_entry->second.body;
230  goto_programt::targett main_call=start.instructions.begin();
231  for(goto_programt::targett end=start.instructions.end();
232  main_call!=end;
233  ++main_call)
234  {
235  //Turn into skip instr. the INPUT(argc ...) instruction
236  if (main_call->is_other() &&
237  main_call->get_other().get_statement() == ID_input &&
238  "argc\'" == id2string(to_symbol_expr(
239  main_call->get_other().op1()).get_identifier())) {
240  main_call->turn_into_skip();
241  }
242 
243  //Turn into skip instr. the ASSUME(argc ...) instruction
244  if(main_call->is_assume() &&
245  "argc\'" == id2string(to_symbol_expr(
246  main_call->condition().operands()[0]).get_identifier())){
247 
248  main_call->turn_into_skip();
249  }
250 
251  if(main_call->is_function_call())
252  {
253  const exprt &func = main_call->call_function();
254  if(func.id()==ID_symbol &&
255  to_symbol_expr(func).get_identifier()==main_symbol.name)
256  break;
257  }
258  }
259  POSTCONDITION(main_call!=start.instructions.end());
260 
261  start.insert_before_swap(main_call, init_instructions);
262 
263  // update counters etc.
264  remove_skip(start);
265 
266  return false;
267 }
bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
bool parse(std::istream &instream, const std::string &path) override
std::vector< parametert > parameterst
Definition: std_types.h:541
const parameterst & parameters() const
Definition: std_types.h:655
optionalt< std::string > main
Definition: config.h:326
struct configt::ansi_ct ansi_c
Base class for all expressions.
Definition: expr.h:54
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::iterator targett
Definition: goto_program.h:592
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt mode
Language mode.
Definition: symbol.h:49
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Program Transformation.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
bool model_argc_argv(goto_modelt &goto_model, const std::list< std::string > &argv_args, bool model_argv, message_handlert &message_handler)
Set up argv to user-specified values (when model_argv is FALSE) or (when model_argv is TRUE) set up a...
std::string escape_char(std::string input_string, std::string find_substring, std::string replace_substring)
Initialize command line arguments.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
const codet & to_code(const exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
preprocessort preprocessor
Definition: config.h:233
Author: Diffblue Ltd.