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 
40  goto_modelt &goto_model,
41  unsigned max_argc,
42  message_handlert &message_handler)
43 {
44  messaget message(message_handler);
45  const namespacet ns(goto_model.symbol_table);
46 
47  if(!goto_model.symbol_table.has_symbol(
48  goto_model.goto_functions.entry_point()))
49  {
50  message.error() << "Linking not done, missing "
51  << goto_model.goto_functions.entry_point()
52  << messaget::eom;
53  return true;
54  }
55 
56  const symbolt &main_symbol=
57  ns.lookup(config.main.empty()?ID_main:config.main);
58 
59  if(main_symbol.mode!=ID_C)
60  {
61  message.error() << "argc/argv modelling is C specific"
62  << messaget::eom;
63  return true;
64  }
65 
66  const code_typet::parameterst &parameters=
67  to_code_type(main_symbol.type).parameters();
68  if(parameters.size()!=2 &&
69  parameters.size()!=3)
70  {
71  message.warning() << "main expected to take 2 or 3 arguments,"
72  << " argc/argv instrumentation skipped"
73  << messaget::eom;
74  return false;
75  }
76 
77  const symbolt &argc_primed = ns.lookup("argc'");
78  symbol_exprt ARGC("ARGC", argc_primed.type);
79  const symbolt &argv_primed = ns.lookup("argv'");
80  symbol_exprt ARGV("ARGV", argv_primed.type);
81 
82  // set the size of ARGV storage to 4096, which matches the minimum
83  // guaranteed by POSIX (_POSIX_ARG_MAX):
84  // http://pubs.opengroup.org/onlinepubs/009695399/basedefs/limits.h.html
85  std::ostringstream oss;
86  oss << "int ARGC;\n"
87  << "char *ARGV[1];\n"
88  << "void " << goto_model.goto_functions.entry_point() << "()\n"
89  << "{\n"
90  << " unsigned next=0u;\n"
91  << " " CPROVER_PREFIX "assume(ARGC>=1);\n"
92  << " " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
93  << " char arg_string[4096];\n"
94  << " " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n"
95  << " for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
96  << " {\n"
97  << " unsigned len;\n"
98  << " " CPROVER_PREFIX "assume(len<4096);\n"
99  << " " CPROVER_PREFIX "assume(next+len<4096);\n"
100  << " " CPROVER_PREFIX "assume(arg_string[next+len]==0);\n"
101  << " ARGV[i]=&(arg_string[next]);\n"
102  << " next+=len+1;\n"
103  << " }\n"
104  << "}";
105  std::istringstream iss(oss.str());
106 
107  ansi_c_languaget ansi_c_language;
108  ansi_c_language.set_message_handler(message_handler);
111  ansi_c_language.parse(iss, "");
113 
114  symbol_tablet tmp_symbol_table;
115  ansi_c_language.typecheck(tmp_symbol_table, "<built-in-library>");
116 
117  goto_programt init_instructions;
118  exprt value=nil_exprt();
119  // locate the body of the newly built start function as well as any
120  // additional declarations we might need; the body will then be
121  // converted and inserted into the start function
122  for(const auto &symbol_pair : tmp_symbol_table.symbols)
123  {
124  // add __CPROVER_assume if necessary (it might exist already)
125  if(
126  symbol_pair.first == CPROVER_PREFIX "assume" ||
127  symbol_pair.first == CPROVER_PREFIX "input")
128  goto_model.symbol_table.add(symbol_pair.second);
129  else if(symbol_pair.first == goto_model.goto_functions.entry_point())
130  {
131  value = symbol_pair.second.value;
132 
134  replace.insert(ARGC, ns.lookup("argc'").symbol_expr());
135  replace.insert(ARGV, ns.lookup("argv'").symbol_expr());
136  replace(value);
137  }
138  else if(
139  has_prefix(
140  id2string(symbol_pair.first),
141  id2string(goto_model.goto_functions.entry_point()) + "::") &&
142  goto_model.symbol_table.add(symbol_pair.second))
143  UNREACHABLE;
144  }
145  POSTCONDITION(value.is_not_nil());
146 
147  goto_convert(
148  to_code(value),
149  goto_model.symbol_table,
150  init_instructions,
151  message_handler,
152  main_symbol.mode);
153 
154  Forall_goto_program_instructions(it, init_instructions)
155  {
156  it->source_location.set_file("<built-in-library>");
157  it->function=goto_model.goto_functions.entry_point();
158  }
159 
160  goto_functionst::function_mapt::iterator start_entry=
161  goto_model.goto_functions.function_map.find(
162  goto_model.goto_functions.entry_point());
163 
165  start_entry!=goto_model.goto_functions.function_map.end() &&
166  start_entry->second.body_available(),
167  "entry point expected to have a body");
168 
169  goto_programt &start=start_entry->second.body;
170  goto_programt::targett main_call=start.instructions.begin();
171  for(goto_programt::targett end=start.instructions.end();
172  main_call!=end;
173  ++main_call)
174  {
175  if(main_call->is_function_call())
176  {
177  const exprt &func=
178  to_code_function_call(main_call->code).function();
179  if(func.id()==ID_symbol &&
180  to_symbol_expr(func).get_identifier()==main_symbol.name)
181  break;
182  }
183  }
184  POSTCONDITION(main_call!=start.instructions.end());
185 
186  start.insert_before_swap(main_call, init_instructions);
187 
188  // update counters etc.
189  remove_skip(start);
190 
191  return false;
192 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:78
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
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:485
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
configt::main
std::string main
Definition: config.h:172
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
replace_symbol.h
model_argc_argv
bool model_argc_argv(goto_modelt &goto_model, unsigned max_argc, message_handlert &message_handler)
Set up argv with up to max_argc pointers into an array of 4096 bytes.
Definition: model_argc_argv.cpp:39
configt::ansi_ct::preprocessort
preprocessort
Definition: config.h:117
prefix.h
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:65
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
invariant.h
messaget::eom
static eomt eom
Definition: message.h:284
goto_convert.h
configt::ansi_c
struct configt::ansi_ct ansi_c
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
namespace.h
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1931
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:386
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:119
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:454
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
message_handlert
Definition: message.h:24
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
cprover_prefix.h
config
configt config
Definition: config.cpp:24
configt::ansi_ct::preprocessort::NONE
@ NONE
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
ansi_c_language.h
ansi_c_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Definition: ansi_c_language.cpp:52
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
unchecked_replace_symbolt
Definition: replace_symbol.h:98
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
config.h
model_argc_argv.h
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
symbol_table.h
Author: Diffblue Ltd.
remove_skip.h
message.h
messaget::warning
mstreamt & warning() const
Definition: message.h:391
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
ansi_c_languaget
Definition: ansi_c_language.h:34
ansi_c_languaget::typecheck
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
Definition: ansi_c_language.cpp:106
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_function_callt::function
exprt & function()
Definition: std_code.h:1099