Skip to content

Commit b1be6d1

Browse files
kroeningkroening
committed
SMV: word types
This adds support for NuSMV's signed and unsigned word types, mapped to signedbv/unsignedbv.
1 parent 29491d5 commit b1be6d1

File tree

6 files changed

+129
-24
lines changed

6 files changed

+129
-24
lines changed

‎regression/smv/word/basic1.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
basic1.smv
3+
--bound 0 --trace
4+
^ s1 = 123 \(01111011\)$
5+
^ u1 = 123 \(01111011\)$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring

‎regression/smv/word/basic1.smv

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
MODULE main
2+
3+
VAR u1 : word[8];
4+
5+
ASSIGN u1 := uwconst(123, 8);
6+
7+
VAR s1 : signed word[8];
8+
9+
ASSIGN s1 := swconst(123, 8);
10+
11+
SPEC FALSE

‎src/hw_cbmc_irep_ids.h

+7
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,19 @@ IREP_ID_ONE(F)
1717
IREP_ID_ONE(E)
1818
IREP_ID_ONE(G)
1919
IREP_ID_ONE(X)
20+
IREP_ID_ONE(smv_extend)
2021
IREP_ID_ONE(smv_next)
2122
IREP_ID_ONE(smv_iff)
2223
IREP_ID_TWO(C_smv_iff, "#smv_iff")
24+
IREP_ID_ONE(smv_resize)
2325
IREP_ID_ONE(smv_setin)
2426
IREP_ID_ONE(smv_setnotin)
27+
IREP_ID_ONE(smv_signed_cast)
28+
IREP_ID_ONE(smv_sizeof)
29+
IREP_ID_ONE(smv_swconst)
2530
IREP_ID_ONE(smv_union)
31+
IREP_ID_ONE(smv_unsigned_cast)
32+
IREP_ID_ONE(smv_uwconst)
2633
IREP_ID_ONE(sva_accept_on)
2734
IREP_ID_ONE(sva_reject_on)
2835
IREP_ID_ONE(sva_sync_accept_on)

‎src/smvlang/expr2smv.cpp

+27-6
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
88

99
#include "expr2smv.h"
1010

11+
#include <util/arith_tools.h>
12+
#include <util/bitvector_types.h>
1113
#include <util/lispexpr.h>
1214
#include <util/lispirep.h>
1315
#include <util/namespace.h>
@@ -101,7 +103,7 @@ class expr2smvt
101103
precedencet &precedence);
102104

103105
bool convert_constant(
104-
const exprt &src,
106+
const constant_exprt &,
105107
std::string &dest,
106108
precedencet &precedence);
107109

@@ -440,14 +442,13 @@ Function: expr2smvt::convert_constant
440442
\*******************************************************************/
441443

442444
bool expr2smvt::convert_constant(
443-
const exprt &src,
445+
const constant_exprt &src,
444446
std::string &dest,
445447
precedencet &precedence)
446448
{
447449
precedence = precedencet::MAX;
448450

449-
const typet &type=src.type();
450-
const std::string &value=src.get_string(ID_value);
451+
const typet &type = src.type();
451452

452453
if(type.id()==ID_bool)
453454
{
@@ -460,7 +461,17 @@ bool expr2smvt::convert_constant(
460461
type.id()==ID_natural ||
461462
type.id()==ID_range ||
462463
type.id()==ID_enumeration)
463-
dest=value;
464+
{
465+
dest = id2string(src.get_value());
466+
}
467+
else if(type.id() == ID_signedbv || type.id() == ID_unsignedbv)
468+
{
469+
auto value_int = numeric_cast_v<mp_integer>(src);
470+
auto sign_specifier = type.id() == ID_signedbv ? 's' : 'u';
471+
auto word_width = to_bitvector_type(type).width();
472+
dest = std::string("0") + sign_specifier + 'd' +
473+
std::to_string(word_width) + '_' + integer2string(value_int);
474+
}
464475
else
465476
return convert_norep(src, dest, precedence);
466477

@@ -585,7 +596,7 @@ bool expr2smvt::convert(
585596
return convert_next_symbol(src, dest, precedence);
586597

587598
else if(src.id()==ID_constant)
588-
return convert_constant(src, dest, precedence);
599+
return convert_constant(to_constant_expr(src), dest, precedence);
589600

590601
else if(src.id()=="smv_nondet_choice")
591602
return convert_nondet_choice(src, dest, precedence);
@@ -707,6 +718,16 @@ bool type2smv(const typet &type, std::string &code, const namespacet &ns)
707718
code+=')';
708719
}
709720
}
721+
else if(type.id() == ID_signedbv)
722+
{
723+
code =
724+
"signed word[" + std::to_string(to_signedbv_type(type).width()) + ']';
725+
}
726+
else if(type.id() == ID_unsignedbv)
727+
{
728+
code =
729+
"unsigned word[" + std::to_string(to_unsignedbv_type(type).width()) + ']';
730+
}
710731
else
711732
return true;
712733

‎src/smvlang/parser.y

+22
Original file line numberDiff line numberDiff line change
@@ -403,6 +403,21 @@ simple_type_specifier:
403403
stack_type($$).add_subtype()=stack_type($6);
404404
}
405405
| boolean_Token { init($$, ID_bool); }
406+
| word_Token '[' NUMBER_Token ']'
407+
{
408+
init($$, ID_unsignedbv);
409+
stack_type($$).set(ID_width, stack_expr($3).id());
410+
}
411+
| signed_Token word_Token '[' NUMBER_Token ']'
412+
{
413+
init($$, ID_signedbv);
414+
stack_type($$).set(ID_width, stack_expr($4).id());
415+
}
416+
| unsigned_Token word_Token '[' NUMBER_Token ']'
417+
{
418+
init($$, ID_unsignedbv);
419+
stack_type($$).set(ID_width, stack_expr($4).id());
420+
}
406421
| '{' enum_list '}' { $$=$2; }
407422
| NUMBER_Token DOTDOT_Token NUMBER_Token
408423
{
@@ -630,6 +645,13 @@ term : variable_name
630645
| term union_Token term { binary($$, $1, ID_smv_union, $3); }
631646
| term IN_Token term { binary($$, $1, ID_smv_setin, $3); }
632647
| term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3); }
648+
| extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
649+
| resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
650+
| signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); }
651+
| sizeof_Token '(' term ')' { init($$, ID_smv_sizeof); mto($$, $3); }
652+
| swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); }
653+
| unsigned_Token '(' term ')' { init($$, ID_smv_unsigned_cast); mto($$, $3); }
654+
| uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); }
633655
;
634656

635657
formula_list: formula { init($$); mto($$, $1); }

‎src/smvlang/smv_typecheck.cpp

+53-18
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "smv_typecheck.h"
1010

1111
#include <util/arith_tools.h>
12+
#include <util/bitvector_types.h>
1213
#include <util/expr_util.h>
1314
#include <util/mathematical_expr.h>
1415
#include <util/namespace.h>
@@ -565,7 +566,15 @@ typet smv_typecheckt::type_union(
565566

566567
if(type2.is_nil())
567568
return type1;
568-
569+
570+
if(
571+
type1.id() == ID_signedbv || type1.id() == ID_unsignedbv ||
572+
type2.id() == ID_signedbv || type2.id() == ID_unsignedbv)
573+
{
574+
throw errort() << "no type union for types" << to_string(type1) << " and "
575+
<< to_string(type2);
576+
}
577+
569578
// both enums?
570579
if(type1.id()==ID_enumeration && type2.id()==ID_enumeration)
571580
{
@@ -1033,6 +1042,26 @@ void smv_typecheckt::typecheck_expr_rec(
10331042
{
10341043
expr.type()=bool_typet();
10351044
}
1045+
else if(expr.id() == ID_smv_swconst)
1046+
{
1047+
auto &binary_expr = to_binary_expr(expr);
1048+
auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.op1()));
1049+
auto type = signedbv_typet{bits};
1050+
auto value =
1051+
numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.op0()));
1052+
expr =
1053+
from_integer(value, type).with_source_location(expr.source_location());
1054+
}
1055+
else if(expr.id() == ID_smv_uwconst)
1056+
{
1057+
auto &binary_expr = to_binary_expr(expr);
1058+
auto bits = numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.op1()));
1059+
auto type = unsignedbv_typet{bits};
1060+
auto value =
1061+
numeric_cast_v<mp_integer>(to_constant_expr(binary_expr.op0()));
1062+
expr =
1063+
from_integer(value, type).with_source_location(expr.source_location());
1064+
}
10361065
else
10371066
{
10381067
throw errort().with_location(expr.find_source_location())
@@ -1061,30 +1090,36 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type)
10611090

10621091
if(expr.type() != type)
10631092
{
1064-
smv_ranget e=convert_type(expr.type());
1065-
smv_ranget t=convert_type(type);
1066-
1067-
if(e.is_contained_in(t) && expr.type().id() != ID_enumeration)
1093+
if(type.id() == ID_signedbv || type.id() == ID_unsignedbv)
10681094
{
1069-
if(e.is_singleton())
1095+
}
1096+
else
1097+
{
1098+
smv_ranget e = convert_type(expr.type());
1099+
smv_ranget t = convert_type(type);
1100+
1101+
if(e.is_contained_in(t) && expr.type().id() != ID_enumeration)
10701102
{
1071-
if(type.id()==ID_bool)
1103+
if(e.is_singleton())
10721104
{
1073-
if(e.from==0)
1074-
expr=false_exprt();
1105+
if(type.id() == ID_bool)
1106+
{
1107+
if(e.from == 0)
1108+
expr = false_exprt();
1109+
else
1110+
expr = true_exprt();
1111+
}
10751112
else
1076-
expr=true_exprt();
1113+
{
1114+
expr = exprt(ID_constant, type);
1115+
expr.set(ID_value, integer2string(e.from));
1116+
}
10771117
}
10781118
else
1079-
{
1080-
expr=exprt(ID_constant, type);
1081-
expr.set(ID_value, integer2string(e.from));
1082-
}
1083-
}
1084-
else
1085-
expr = typecast_exprt{expr, type};
1119+
expr = typecast_exprt{expr, type};
10861120

1087-
return;
1121+
return;
1122+
}
10881123
}
10891124

10901125
throw errort().with_location(expr.find_source_location())

0 commit comments

Comments
 (0)