Skip to content

Commit 897da60

Browse files
tautschnigtautschnig
authored
Merge pull request #1093 from diffblue/smv_expr_h
SMV: introduce classes for `extend`, `resize`, `signed`, `unsigned`
2 parents 156e76c + 59b4d9a commit 897da60

File tree

4 files changed

+206
-9
lines changed

4 files changed

+206
-9
lines changed

‎src/smvlang/Makefile

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
SRC = smv_language.cpp \
1+
SRC = smv_expr.cpp \
2+
smv_language.cpp \
23
smv_parser.cpp \
34
smv_typecheck.cpp \
45
expr2smv.cpp \

‎src/smvlang/smv_expr.cpp

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/*******************************************************************\
2+
3+
Module: SMV Expressions
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "smv_expr.h"
10+
11+
#include <util/arith_tools.h>
12+
#include <util/mathematical_types.h>
13+
14+
smv_resize_exprt::smv_resize_exprt(exprt __op, std::size_t __size, typet __type)
15+
: smv_resize_exprt{
16+
std::move(__op),
17+
from_integer(__size, natural_typet{}),
18+
std::move(__type)}
19+
{
20+
}
21+
22+
smv_extend_exprt::smv_extend_exprt(exprt __op, std::size_t __size, typet __type)
23+
: smv_extend_exprt{
24+
std::move(__op),
25+
from_integer(__size, natural_typet{}),
26+
std::move(__type)}
27+
{
28+
}

‎src/smvlang/smv_expr.h

+167
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,167 @@
1+
/*******************************************************************\
2+
3+
Module: SMV Expressions
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_SMV_EXPR_H
10+
#define CPROVER_SMV_EXPR_H
11+
12+
#include <util/std_expr.h>
13+
14+
class smv_resize_exprt : public binary_exprt
15+
{
16+
public:
17+
smv_resize_exprt(exprt __op, constant_exprt __size, typet __type)
18+
: binary_exprt{
19+
std::move(__op),
20+
ID_smv_resize,
21+
std::move(__size),
22+
std::move(__type)}
23+
{
24+
}
25+
26+
smv_resize_exprt(exprt __op, std::size_t __size, typet);
27+
28+
const exprt &op() const
29+
{
30+
return op0();
31+
}
32+
33+
exprt &op()
34+
{
35+
return op0();
36+
}
37+
38+
const constant_exprt &size() const
39+
{
40+
return static_cast<const constant_exprt &>(op1());
41+
}
42+
43+
constant_exprt &size()
44+
{
45+
return static_cast<constant_exprt &>(op1());
46+
}
47+
48+
protected:
49+
using binary_exprt::op0;
50+
using binary_exprt::op1;
51+
};
52+
53+
inline const smv_resize_exprt &to_smv_resize_expr(const exprt &expr)
54+
{
55+
PRECONDITION(expr.id() == ID_smv_resize);
56+
smv_resize_exprt::check(expr);
57+
return static_cast<const smv_resize_exprt &>(expr);
58+
}
59+
60+
inline smv_resize_exprt &to_smv_resize_expr(exprt &expr)
61+
{
62+
PRECONDITION(expr.id() == ID_smv_resize);
63+
smv_resize_exprt::check(expr);
64+
return static_cast<smv_resize_exprt &>(expr);
65+
}
66+
67+
class smv_extend_exprt : public binary_exprt
68+
{
69+
public:
70+
smv_extend_exprt(exprt __op, constant_exprt __size, typet __type)
71+
: binary_exprt{
72+
std::move(__op),
73+
ID_smv_extend,
74+
std::move(__size),
75+
std::move(__type)}
76+
{
77+
}
78+
79+
smv_extend_exprt(exprt __op, std::size_t __size, typet);
80+
81+
const exprt &op() const
82+
{
83+
return op0();
84+
}
85+
86+
exprt &op()
87+
{
88+
return op0();
89+
}
90+
91+
const constant_exprt &size() const
92+
{
93+
return static_cast<const constant_exprt &>(op1());
94+
}
95+
96+
constant_exprt &size()
97+
{
98+
return static_cast<constant_exprt &>(op1());
99+
}
100+
101+
protected:
102+
using binary_exprt::op0;
103+
using binary_exprt::op1;
104+
};
105+
106+
inline const smv_extend_exprt &to_smv_extend_expr(const exprt &expr)
107+
{
108+
PRECONDITION(expr.id() == ID_smv_extend);
109+
smv_extend_exprt::check(expr);
110+
return static_cast<const smv_extend_exprt &>(expr);
111+
}
112+
113+
inline smv_extend_exprt &to_smv_extend_expr(exprt &expr)
114+
{
115+
PRECONDITION(expr.id() == ID_smv_extend);
116+
smv_extend_exprt::check(expr);
117+
return static_cast<smv_extend_exprt &>(expr);
118+
}
119+
120+
class smv_unsigned_cast_exprt : public unary_exprt
121+
{
122+
public:
123+
smv_unsigned_cast_exprt(exprt __op, typet __type)
124+
: unary_exprt{ID_smv_unsigned_cast, std::move(__op), std::move(__type)}
125+
{
126+
}
127+
};
128+
129+
inline const smv_unsigned_cast_exprt &
130+
to_smv_unsigned_cast_expr(const exprt &expr)
131+
{
132+
PRECONDITION(expr.id() == ID_smv_unsigned_cast);
133+
smv_unsigned_cast_exprt::check(expr);
134+
return static_cast<const smv_unsigned_cast_exprt &>(expr);
135+
}
136+
137+
inline smv_unsigned_cast_exprt &to_smv_unsigned_cast_expr(exprt &expr)
138+
{
139+
PRECONDITION(expr.id() == ID_smv_unsigned_cast);
140+
smv_unsigned_cast_exprt::check(expr);
141+
return static_cast<smv_unsigned_cast_exprt &>(expr);
142+
}
143+
144+
class smv_signed_cast_exprt : public unary_exprt
145+
{
146+
public:
147+
smv_signed_cast_exprt(exprt __op, typet __type)
148+
: unary_exprt{ID_smv_signed_cast, std::move(__op), std::move(__type)}
149+
{
150+
}
151+
};
152+
153+
inline const smv_signed_cast_exprt &to_smv_signed_cast_expr(const exprt &expr)
154+
{
155+
PRECONDITION(expr.id() == ID_smv_signed_cast);
156+
smv_signed_cast_exprt::check(expr);
157+
return static_cast<const smv_signed_cast_exprt &>(expr);
158+
}
159+
160+
inline smv_signed_cast_exprt &to_smv_signed_cast_expr(exprt &expr)
161+
{
162+
PRECONDITION(expr.id() == ID_smv_signed_cast);
163+
smv_signed_cast_exprt::check(expr);
164+
return static_cast<smv_signed_cast_exprt &>(expr);
165+
}
166+
167+
#endif // CPROVER_SMV_EXPR_H

‎src/smvlang/smv_typecheck.cpp

+9-8
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/typecheck.h>
1818

1919
#include "expr2smv.h"
20+
#include "smv_expr.h"
2021
#include "smv_range.h"
2122

2223
#include <algorithm>
@@ -1202,7 +1203,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
12021203
else if(expr.id() == ID_smv_unsigned_cast)
12031204
{
12041205
// a reinterpret cast
1205-
auto &op = to_unary_expr(expr).op();
1206+
auto &op = to_smv_unsigned_cast_expr(expr).op();
12061207
typecheck_expr_rec(op, mode);
12071208
if(op.type().id() == ID_signedbv)
12081209
expr.type() = unsignedbv_typet{to_signedbv_type(op.type()).get_width()};
@@ -1215,7 +1216,7 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
12151216
else if(expr.id() == ID_smv_signed_cast)
12161217
{
12171218
// a reinterpret cast
1218-
auto &op = to_unary_expr(expr).op();
1219+
auto &op = to_smv_signed_cast_expr(expr).op();
12191220
typecheck_expr_rec(op, mode);
12201221
if(op.type().id() == ID_unsignedbv)
12211222
expr.type() = signedbv_typet{to_unsignedbv_type(op.type()).get_width()};
@@ -1248,21 +1249,21 @@ void smv_typecheckt::lower_node(exprt &expr) const
12481249
{
12491250
if(expr.id() == ID_smv_extend)
12501251
{
1251-
auto &binary = to_binary_expr(expr);
1252-
expr = typecast_exprt{binary.lhs(), expr.type()};
1252+
auto &smv_extend = to_smv_extend_expr(expr);
1253+
expr = typecast_exprt{smv_extend.lhs(), smv_extend.type()};
12531254
}
12541255
else if(expr.id() == ID_smv_resize)
12551256
{
1256-
auto &binary = to_binary_expr(expr);
1257-
expr = typecast_exprt{binary.lhs(), expr.type()};
1257+
auto &smv_resize = to_smv_resize_expr(expr);
1258+
expr = typecast_exprt{smv_resize.lhs(), smv_resize.type()};
12581259
}
12591260
else if(expr.id() == ID_smv_signed_cast)
12601261
{
1261-
expr = typecast_exprt{to_unary_expr(expr).op(), expr.type()};
1262+
expr = typecast_exprt{to_smv_signed_cast_expr(expr).op(), expr.type()};
12621263
}
12631264
else if(expr.id() == ID_smv_unsigned_cast)
12641265
{
1265-
expr = typecast_exprt{to_unary_expr(expr).op(), expr.type()};
1266+
expr = typecast_exprt{to_smv_unsigned_cast_expr(expr).op(), expr.type()};
12661267
}
12671268
}
12681269

0 commit comments

Comments
 (0)