cprover
goto_program_irep.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: goto_programt -> irep conversion
4 
5 Author: CM Wintersteiger
6 
7 Date: May 2007
8 
9 \*******************************************************************/
10 
13 
14 #include "goto_program_irep.h"
15 
16 #include <iostream>
17 
18 #include <util/string2int.h>
19 
20 void convert(const goto_programt::instructiont &instruction, irept &irep)
21 {
22  irep.set(ID_code, instruction.code);
23 
24  if(instruction.function!="")
25  irep.set(ID_function, instruction.function);
26 
27  if(instruction.source_location.is_not_nil())
28  irep.set(ID_location, instruction.source_location);
29 
30  irep.set(ID_type, (long) instruction.type);
31 
32  irep.set(ID_guard, instruction.guard);
33 
34  if(!instruction.targets.empty())
35  {
36  irept &tgts=irep.add(ID_targets);
37  for(const auto &target : instruction.targets)
38  {
39  irept t(std::to_string(target->location_number));
40  tgts.move_to_sub(t);
41  }
42  }
43 
44  if(!instruction.labels.empty())
45  {
46  irept &lbls = irep.add(ID_labels);
47  irept::subt &subs = lbls.get_sub();
48  subs.reserve(instruction.labels.size());
49  for(const auto &label : instruction.labels)
50  {
51  subs.push_back(irept(label));
52  }
53  }
54 }
55 
56 void convert(
57  const irept &irep,
58  goto_programt::instructiont &instruction)
59 {
60  instruction.code=static_cast<const codet &>(irep.find(ID_code));
61  instruction.function = irep.find(ID_function).id();
62  instruction.source_location=
63  static_cast<const source_locationt &>(irep.find(ID_location));
64  instruction.type = static_cast<goto_program_instruction_typet>(
65  unsafe_string2unsigned(irep.find(ID_type).id_string()));
66  instruction.guard = static_cast<const exprt&>(irep.find(ID_guard));
67 
68  // don't touch the targets, the goto_programt conversion does that
69 
70  const irept &lbls=irep.find(ID_labels);
71  const irept::subt &lsubs=lbls.get_sub();
72  for(const auto &lsub : lsubs)
73  instruction.labels.push_back(lsub.id());
74 }
75 
76 void convert(const goto_programt &program, irept &irep)
77 {
78  irep.id("goto-program");
79  irep.get_sub().reserve(program.instructions.size());
81  {
82  irep.get_sub().push_back(irept());
83  convert(*it, irep.get_sub().back());
84  }
85 }
86 
87 void convert(const irept &irep, goto_programt &program)
88 {
89  assert(irep.id()=="goto-program");
90 
91  program.instructions.clear();
92 
93  std::list< std::list<unsigned> > number_targets_list;
94 
95  // convert instructions back
96  const irept::subt &subs = irep.get_sub();
97  for(irept::subt::const_iterator it=subs.begin();
98  it!=subs.end();
99  it++)
100  {
101  program.instructions.push_back(goto_programt::instructiont());
102  convert(*it, program.instructions.back());
103 
104  number_targets_list.push_back(std::list<unsigned>());
105  const irept &targets=it->find(ID_targets);
106  const irept::subt &tsubs=targets.get_sub();
107  for(const auto &tsub : tsubs)
108  number_targets_list.back().push_back(
109  unsafe_string2unsigned(tsub.id_string()));
110  }
111 
112  program.compute_location_numbers();
113 
114  // resolve targets
115  std::list< std::list<unsigned> >::iterator nit=
116  number_targets_list.begin();
117  for(goto_programt::instructionst::iterator lit=
118  program.instructions.begin();
119  lit!=program.instructions.end() && nit!=number_targets_list.end();
120  lit++, nit++)
121  {
122  for(const unsigned t : *nit)
123  {
124  goto_programt::targett fit=program.instructions.begin();
125  for( ; fit!=program.instructions.end(); fit++)
126  {
127  if(fit->location_number==t)
128  {
129  lit->targets.push_back(fit);
130  break;
131  }
132  }
133 
134  if(fit==program.instructions.end())
135  {
136  std::cout << "Warning: could not resolve target link "
137  << "during irep->goto_program translation.\n";
138  throw 0;
139  }
140  }
141  }
142 
143  program.update();
144 }
goto_program_instruction_typet
The type of an instruction in a GOTO program.
void update()
Update all indices.
std::vector< irept > subt
Definition: irep.h:91
void move_to_sub(irept &irep)
Definition: irep.cpp:204
goto_programt -> irep conversion
instructionst instructions
The list of instructions in the goto program.
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
void compute_location_numbers(unsigned &nr)
Compute location numbers.
subt & get_sub()
Definition: irep.h:245
const irep_idt & id() const
Definition: irep.h:189
Base class for tree-like data structures with sharing.
Definition: irep.h:87
void convert(const goto_programt::instructiont &instruction, irept &irep)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Base class for all expressions.
Definition: expr.h:46
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const std::string & id_string() const
Definition: irep.h:192
A statement in a programming language.
Definition: std_code.h:19
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214