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/message.h>
20 #include <util/namespace.h>
21 #include <util/config.h>
22 #include <util/replace_symbol.h>
23 #include <util/symbol_table.h>
24 #include <util/prefix.h>
25 
26 #include <ansi-c/ansi_c_language.h>
27 
31 
33  symbol_tablet &symbol_table,
34  goto_functionst &goto_functions,
35  unsigned max_argc,
36  message_handlert &message_handler)
37 {
38  messaget message(message_handler);
39  const namespacet ns(symbol_table);
40 
41  const symbolt *init_symbol=nullptr;
42  if(ns.lookup(CPROVER_PREFIX "initialize", init_symbol))
43  {
44  message.error() << "Linking not done, missing "
45  << CPROVER_PREFIX "initialize" << messaget::eom;
46  return true;
47  }
48 
49  if(init_symbol->mode!=ID_C)
50  {
51  message.error() << "argc/argv modelling is C specific"
52  << messaget::eom;
53  return true;
54  }
55 
56  goto_functionst::function_mapt::iterator init_entry=
57  goto_functions.function_map.find(CPROVER_PREFIX "initialize");
58  assert(
59  init_entry!=goto_functions.function_map.end() &&
60  init_entry->second.body_available());
61 
62  goto_programt &init=init_entry->second.body;
63  goto_programt::targett init_end=init.instructions.end();
64  --init_end;
65  assert(init_end->is_end_function());
66  assert(init_end!=init.instructions.begin());
67  --init_end;
68 
69  const symbolt &main_symbol=
70  ns.lookup(config.main.empty()?ID_main:config.main);
71 
72  const code_typet::parameterst &parameters=
73  to_code_type(main_symbol.type).parameters();
74  if(parameters.size()!=2 &&
75  parameters.size()!=3)
76  {
77  message.warning() << "main expected to take 2 or 3 arguments,"
78  << " argc/argv instrumentation skipped"
79  << messaget::eom;
80  return false;
81  }
82 
83  // set the size of ARGV storage to 4096, which matches the minimum
84  // guaranteed by POSIX (_POSIX_ARG_MAX):
85  // http://pubs.opengroup.org/onlinepubs/009695399/basedefs/limits.h.html
86  std::ostringstream oss;
87  oss << "int ARGC;\n"
88  << "char *ARGV[1];\n"
89  << "void " CPROVER_PREFIX "initialize()\n"
90  << "{\n"
91  << " unsigned next=0u;\n"
92  << " " CPROVER_PREFIX "assume(ARGC>=1);\n"
93  << " " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
94  << " " CPROVER_PREFIX "thread_local static char arg_string[4096];\n"
95  << " for(unsigned i=0u; 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 tmp;
118  exprt value=nil_exprt();
119  // locate the body of the newly built initialize function as well
120  // as any additional declarations we might need; the body will then
121  // be converted and appended to the existing initialize function
122  forall_symbols(it, tmp_symbol_table.symbols)
123  {
124  // add __CPROVER_assume if necessary (it might exist already)
125  if(it->first==CPROVER_PREFIX "assume")
126  symbol_table.add(it->second);
127  else if(it->first==CPROVER_PREFIX "initialize")
128  {
129  value=it->second.value;
130 
131  replace_symbolt replace;
132  replace.insert("ARGC", ns.lookup("argc'").symbol_expr());
133  replace.insert("ARGV", ns.lookup("argv'").symbol_expr());
134  replace(value);
135  }
136  else if(has_prefix(id2string(it->first),
137  CPROVER_PREFIX "initialize::") &&
138  symbol_table.add(it->second))
139  assert(false);
140  }
141 
142  assert(value.is_not_nil());
143  goto_convert(
144  to_code(value),
145  symbol_table,
146  tmp,
147  message_handler);
149  {
150  it->source_location.set_file("<built-in-library>");
151  it->function=CPROVER_PREFIX "initialize";
152  }
153  init.insert_before_swap(init_end, tmp);
154 
155  // update counters etc.
156  remove_skip(init);
157  init.compute_loop_numbers();
158  goto_functions.update();
159 
160  return false;
161 }
162 
mstreamt & warning()
Definition: message.h:228
struct configt::ansi_ct ansi_c
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
Initialize command line arguments.
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:55
Goto Programs with Functions.
std::vector< parametert > parameterst
Definition: std_types.h:829
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
preprocessort preprocessor
Definition: config.h:109
symbolst symbols
Definition: symbol_table.h:57
The NIL expression.
Definition: std_expr.h:3764
std::string main
Definition: config.h:147
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
Program Transformation.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
mstreamt & error()
Definition: message.h:223
void insert(const irep_idt &identifier, const exprt &expr)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
Program Transformation.
bool model_argc_argv(symbol_tablet &symbol_table, goto_functionst &goto_functions, unsigned max_argc, message_handlert &message_handler)