cprover
mm2cpp.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "mm2cpp.h"
10 
11 #include <ostream>
12 
13 #include <util/std_code.h>
14 
15 class mm2cppt
16 {
17 public:
18  explicit mm2cppt(std::ostream &_out):out(_out)
19  {
20  }
21 
23  void operator()(const irept &);
24 
25 protected:
26  std::ostream &out;
27  typedef std::map<irep_idt, exprt> let_valuest;
28  let_valuest let_values;
29 
30  static std::string text2c(const irep_idt &src);
31  void instruction2cpp(const codet &code, unsigned indent);
32  void check_acyclic(const exprt &, unsigned indent);
33 };
34 
35 std::string mm2cppt::text2c(const irep_idt &src)
36 {
37  std::string result;
38  result.reserve(src.size());
39 
40  for(unsigned i=0; i<src.size(); i++)
41  {
42  char ch=src[i];
43  if(isalnum(ch))
44  result+=ch;
45  else
46  result+='_';
47  }
48 
49  return result;
50 }
51 
52 void mm2cppt::check_acyclic(const exprt &expr, unsigned indent)
53 {
54  if(expr.id()==ID_symbol)
55  {
56  const irep_idt &identifier=expr.get(ID_identifier);
57  let_valuest::const_iterator v_it=let_values.find(identifier);
58  if(v_it!=let_values.end())
59  check_acyclic(v_it->second, indent);
60  else if(identifier=="po")
61  {
62  }
63  else if(identifier=="rf")
64  {
65  }
66  else if(identifier=="co")
67  {
68  }
69  else if(identifier=="loc")
70  {
71  }
72  else if(identifier=="int")
73  {
74  }
75  else if(identifier=="ext")
76  {
77  }
78  else if(identifier=="id")
79  {
80  }
81  else if(identifier=="R")
82  {
83  }
84  else if(identifier=="W")
85  {
86  }
87  else if(identifier=="F")
88  {
89  }
90  else if(identifier=="B")
91  {
92  }
93  else if(identifier=="RMW")
94  {
95  }
96  else if(identifier=="rmw")
97  {
98  }
99  else if(identifier=="IW")
100  {
101  }
102  else if(identifier=="FW")
103  {
104  }
105  else if(identifier=="M")
106  {
107  }
108  else if(identifier=="addr")
109  {
110  }
111  else if(identifier=="data")
112  {
113  }
114  else if(identifier=="ctrl")
115  {
116  }
117  else
118  {
119  throw expr.source_location().as_string()+
120  ": unknown identifier `"+id2string(identifier)+"'";
121  }
122  }
123  else if(expr.id()==ID_union)
124  {
125  assert(expr.operands().size()==2);
126  check_acyclic(expr.op0(), indent);
127  check_acyclic(expr.op1(), indent);
128  }
129  else
130  throw "acyclic cannot do "+expr.id_string();
131 }
132 
133 void mm2cppt::instruction2cpp(const codet &code, unsigned indent)
134 {
135  const irep_idt &statement=code.get_statement();
136 
137  if(statement==ID_block)
138  {
139  forall_operands(it, code)
140  {
141  instruction2cpp(to_code(*it), indent+2);
142  }
143  }
144  else if(statement==ID_let)
145  {
146  assert(code.operands().size()==1);
147  const exprt &binding_list=code.op0();
148  forall_operands(it, binding_list)
149  {
150  if(it->id()=="valbinding")
151  {
152  assert(it->operands().size()==2);
153  if(it->op0().id()==ID_symbol)
154  {
155  irep_idt identifier=it->op0().get(ID_identifier);
156  let_values[identifier]=it->op1();
157  }
158  else
159  throw "cannot do tuple valbinding";
160  }
161  else if(it->id()=="funbinding")
162  {
163  throw "cannot do funbinding";
164  }
165  else
166  throw "unknown let binding";
167  }
168  }
169  else if(statement=="check")
170  {
171  assert(code.operands().size()==3);
172  if(code.op0().id()=="acyclic")
173  {
174  check_acyclic(code.op1(), indent);
175  }
176  else
177  {
178  throw "can only do 'acyclic'";
179  }
180  }
181 }
182 
183 void mm2cppt::operator()(const irept &instruction)
184 {
185  out << "// Generated by mmcc\n";
186  out << "// Model: " << model_name << '\n';
187  out << '\n';
188 
189  out << "class memory_model_" << text2c(model_name) << "t\n";
190  out << "{\n";
191  out << "public:\n";
192  out << " void operator()();\n";
193  out << "};\n";
194  out << '\n';
195 
196  out << "void memory_model_" << text2c(model_name) << "t::operator()()\n";
197  out << "{\n";
198  instruction2cpp(to_code(static_cast<const exprt &>(instruction)), 0);
199  out << "}\n";
200  out << '\n';
201 }
202 
203 void mm2cpp(
204  const irep_idt &model_name,
205  const irept &instruction,
206  std::ostream &out)
207 {
208  mm2cppt mm2cpp(out);
209  mm2cpp.model_name=model_name;
210  mm2cpp(instruction);
211 }
const irep_idt & get_statement() const
Definition: std_code.h:37
std::ostream & out
Definition: mm2cpp.cpp:26
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
exprt & op0()
Definition: expr.h:84
let_valuest let_values
Definition: mm2cpp.cpp:28
void mm2cpp(const irep_idt &model_name, const irept &instruction, std::ostream &out)
Definition: mm2cpp.cpp:203
std::string as_string() const
void instruction2cpp(const codet &code, unsigned indent)
Definition: mm2cpp.cpp:133
const irep_idt & id() const
Definition: irep.h:189
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
irep_idt model_name
Definition: mm2cpp.cpp:22
Base class for tree-like data structures with sharing.
Definition: irep.h:87
#define forall_operands(it, expr)
Definition: expr.h:17
size_t size() const
Definition: dstring.h:77
std::map< irep_idt, exprt > let_valuest
Definition: mm2cpp.cpp:27
static std::string text2c(const irep_idt &src)
Definition: mm2cpp.cpp:35
Base class for all expressions.
Definition: expr.h:46
void operator()(const irept &)
Definition: mm2cpp.cpp:183
const source_locationt & source_location() const
Definition: expr.h:142
void check_acyclic(const exprt &, unsigned indent)
Definition: mm2cpp.cpp:52
const std::string & id_string() const
Definition: irep.h:192
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
mm2cppt(std::ostream &_out)
Definition: mm2cpp.cpp:18
A statement in a programming language.
Definition: std_code.h:19
operandst & operands()
Definition: expr.h:70