cprover
replace_async.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Vincent Nimal
6 
7 Date: December 2013
8 
9 \*******************************************************************/
10 
11 
12 #ifndef CPROVER_MUSKETEER_REPLACE_ASYNC_H
13 #define CPROVER_MUSKETEER_REPLACE_ASYNC_H
14 
16 #include <util/std_code.h>
17 
18 class goto_functionst;
19 class namespacet;
20 
22  const namespacet &ns,
23  goto_functionst &goto_functions)
24 {
25  Forall_goto_functions(f_it, goto_functions)
26  {
27  goto_programt &program=f_it->second.body;
28 
30  {
31  const goto_programt::instructiont &instruction=*i_it;
32 
33  if(instruction.is_function_call())
34  {
35  const code_function_callt &fct=to_code_function_call(instruction.code);
36  if(fct.function().id() == ID_symbol)
37  {
38  const symbol_exprt &fsym=to_symbol_expr(fct.function());
39 
40  if(ns.lookup(fsym.get_identifier()).base_name == "pthread_create")
41  {
42  assert(fct.arguments().size()>=4);
43  code_function_callt new_call;
44  /* takes the 3rd argument (pointer to the function to call) */
45  const exprt &fct_name=fct.arguments()[2];
46 
47  if(fct_name.id()==ID_address_of)
48  {
49  /* pointer to function */
50  new_call.function()=
51  to_address_of_expr(fct.arguments()[2]).object();
52  }
53  else
54  {
55  /* other (e.g. local copy) */
56  new_call.function()=fct_name;
57  }
58 
59  new_call.arguments().resize(1);
60  /* takes the 4th argument (argument of the function to call) */
61  new_call.arguments()[0]=fct.arguments()[3];
62 
63  /* __CPROVER_ASYNC labels only evaluated at C parsing time; we
64  reproduce here the effects of the evaluation of this label */
65  i_it->labels.push_front("__CPROVER_ASYNC_0");
66  i_it->clear(START_THREAD);
67  /* CP_AC_0: f(); -> CP_AC_0: start_th; goto 2;
68  1: f(); end_th; 2: ... */
69 
70  goto_programt::targett goto2=program.insert_after(i_it);
71  goto_programt::targett call=program.insert_after(goto2);
72  goto_programt::targett end=program.insert_after(call);
73  goto_programt::targett skip=program.insert_after(end);
74 
75  goto2->make_goto(skip);
76  call->make_function_call(new_call);
77  end->clear(END_THREAD);
78  skip->make_skip();
79  }
80  }
81  }
82  }
83  }
84 }
85 
86 #endif // CPROVER_MUSKETEER_REPLACE_ASYNC_H
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const irep_idt & get_identifier() const
Definition: std_expr.h:120
const irep_idt & id() const
Definition: irep.h:189
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
argumentst & arguments()
Definition: std_code.h:689
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
targett insert_after(const_targett target)
Insertion after the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
void replace_async(const namespacet &ns, goto_functionst &goto_functions)
Definition: replace_async.h:21
Expression to hold a symbol (variable)
Definition: std_expr.h:82
Concrete Goto Program.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700