cprover
Loading...
Searching...
No Matches
model_argc_argv.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Initialize command line arguments
4
5Author: Michael Tautschnig
6
7Date: April 2016
8
9\*******************************************************************/
10
13
14#include "model_argc_argv.h"
15
16#include <util/config.h>
17#include <util/cprover_prefix.h>
18#include <util/invariant.h>
19#include <util/message.h>
20#include <util/namespace.h>
21#include <util/prefix.h>
22#include <util/replace_symbol.h>
23#include <util/symbol_table.h>
24
27
30
31#include <sstream>
32
38std::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()
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"
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 << "extern char " CPROVER_PREFIX "arg_string[4096];\n"
130 << "void " << goto_model.goto_functions.entry_point() << "()\n"
131 << "{\n"
132 << " unsigned next=0u;\n"
133 << " " CPROVER_PREFIX "assume(ARGC>=1);\n"
134 << " " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
135 << " " CPROVER_PREFIX "input(\"arg_string\", \n"
136 << " &" CPROVER_PREFIX "arg_string[0]);\n"
137 << " for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
138 << " {\n"
139 << " unsigned len;\n"
140 << " " CPROVER_PREFIX "assume(len<4096);\n"
141 << " " CPROVER_PREFIX "assume(next+len<4096);\n"
142 << " " CPROVER_PREFIX "assume(\n"
143 << " " CPROVER_PREFIX "arg_string[next+len]==0);\n"
144 << " ARGV[i]=&(" CPROVER_PREFIX "arg_string[next]);\n"
145 << " next+=len+1;\n"
146 << " }\n"
147 << "}";
148 }
149 else
150 { // model_argv = false, set each argv[i] explicitly
151 oss << "int ARGC = " << argc << ";\n"
152 << "char *ARGV[" << argc << "];\n"
153 << "void " << goto_model.goto_functions.entry_point() << "()\n"
154 << "{\n"
155 << "int ARGC = " << argc << ";\n";
156 int i = 0;
157 for(auto &arg : argv_args)
158 {
159 oss << "ARGV[" << i << "]=\"" << escape_char(
161 escape_char(arg, "\\","\\\\"),
162 "\'","\\\'"),
163 "\"","\\\"")
164 << "\";\n";
165 i++;
166 }
167 oss << "}";
168 }
169
170 std::istringstream iss(oss.str());
171
172 ansi_c_languaget ansi_c_language;
175 ansi_c_language.parse(iss, "", message_handler);
177
178 symbol_tablet tmp_symbol_table;
179 ansi_c_language.typecheck(
180 tmp_symbol_table, "<built-in-library>", message_handler);
181
182 goto_programt init_instructions;
183 exprt value=nil_exprt();
184 // locate the body of the newly built start function as well as any
185 // additional declarations we might need; the body will then be
186 // converted and inserted into the start function
187 for(const auto &symbol_pair : tmp_symbol_table.symbols)
188 {
189 // add __CPROVER_assume if necessary (it might exist already)
190 if(
191 symbol_pair.first == CPROVER_PREFIX "assume" ||
192 symbol_pair.first == CPROVER_PREFIX "input" ||
193 symbol_pair.first == CPROVER_PREFIX "arg_string")
194 {
195 goto_model.symbol_table.add(symbol_pair.second);
196 }
197 else if(symbol_pair.first == goto_model.goto_functions.entry_point())
198 {
199 value = symbol_pair.second.value;
200
202 replace.insert(ARGC, ns.lookup("argc'").symbol_expr());
203 replace.insert(ARGV, ns.lookup("argv'").symbol_expr());
204 replace(value);
205 }
206 else if(
208 id2string(symbol_pair.first),
209 id2string(goto_model.goto_functions.entry_point()) + "::") &&
210 goto_model.symbol_table.add(symbol_pair.second))
212 }
213 POSTCONDITION(value.is_not_nil());
214
216 to_code(value),
217 goto_model.symbol_table,
218 init_instructions,
219 message_handler,
220 main_symbol.mode);
221
222 for(auto &instruction : init_instructions.instructions)
223 instruction.source_location_nonconst().set_file("<built-in-library>");
224
225 goto_functionst::function_mapt::iterator start_entry=
226 goto_model.goto_functions.function_map.find(
227 goto_model.goto_functions.entry_point());
228
230 start_entry!=goto_model.goto_functions.function_map.end() &&
231 start_entry->second.body_available(),
232 "entry point expected to have a body");
233
234 goto_programt &start=start_entry->second.body;
235 goto_programt::targett main_call=start.instructions.begin();
236 for(goto_programt::targett end=start.instructions.end();
237 main_call!=end;
238 ++main_call)
239 {
240 //Turn into skip instr. the INPUT(argc ...) instruction
241 if (main_call->is_other() &&
242 main_call->get_other().get_statement() == ID_input &&
243 "argc\'" == id2string(to_symbol_expr(
244 main_call->get_other().op1()).get_identifier())) {
245 main_call->turn_into_skip();
246 }
247
248 //Turn into skip instr. the ASSUME(argc ...) instruction
249 if(main_call->is_assume() &&
250 "argc\'" == id2string(to_symbol_expr(
251 main_call->condition().operands()[0]).get_identifier())){
252
253 main_call->turn_into_skip();
254 }
255
256 if(main_call->is_function_call())
257 {
258 const exprt &func = main_call->call_function();
259 if(func.id()==ID_symbol &&
260 to_symbol_expr(func).get_identifier()==main_symbol.name)
261 break;
262 }
263 }
264 POSTCONDITION(main_call!=start.instructions.end());
265
266 start.insert_before_swap(main_call, init_instructions);
267
268 // update counters etc.
269 remove_skip(start);
270
271 return false;
272}
configt config
Definition config.cpp:25
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
const parameterst & parameters() const
Definition std_types.h:699
std::vector< parametert > parameterst
Definition std_types.h:586
std::optional< std::string > main
Definition config.h:360
struct configt::ansi_ct ansi_c
Base class for all expressions.
Definition expr.h:56
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:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
bool is_not_nil() const
Definition irep.h:372
const irep_idt & id() const
Definition irep.h:388
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
mstreamt & warning() const
Definition message.h:396
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3086
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
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.
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
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
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:44
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)
Escape selected character in specified string with backslashes.
Initialize command line arguments.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#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:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
preprocessort preprocessor
Definition config.h:267
Author: Diffblue Ltd.