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