Skip to content

Commit 64e103f

Browse files
kroeningkroening
committed
SMV: avoid ambiguity when generating binary expression strings
1 parent 6643d61 commit 64e103f

File tree

4 files changed

+142
-31
lines changed

4 files changed

+142
-31
lines changed

‎src/smvlang/expr2smv.cpp

+91-27
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,58 @@ Function: expr2smvt::convert_binary
8888
\*******************************************************************/
8989

9090
expr2smvt::resultt expr2smvt::convert_binary(
91+
const binary_exprt &src,
92+
const std::string &symbol,
93+
precedencet precedence)
94+
{
95+
std::string dest;
96+
97+
{
98+
// lhs
99+
auto lhs_rec = convert_rec(src.lhs());
100+
101+
if(precedence >= lhs_rec.p)
102+
dest += '(';
103+
104+
dest += lhs_rec.s;
105+
106+
if(precedence >= lhs_rec.p)
107+
dest += ')';
108+
}
109+
110+
dest += ' ';
111+
dest += symbol;
112+
dest += ' ';
113+
114+
{
115+
// rhs
116+
auto rhs_rec = convert_rec(src.rhs());
117+
118+
if(precedence >= rhs_rec.p)
119+
dest += '(';
120+
121+
dest += rhs_rec.s;
122+
123+
if(precedence >= rhs_rec.p)
124+
dest += ')';
125+
}
126+
127+
return {precedence, std::move(dest)};
128+
}
129+
130+
/*******************************************************************\
131+
132+
Function: expr2smvt::convert_binary_associative
133+
134+
Inputs:
135+
136+
Outputs:
137+
138+
Purpose:
139+
140+
\*******************************************************************/
141+
142+
expr2smvt::resultt expr2smvt::convert_binary_associative(
91143
const exprt &src,
92144
const std::string &symbol,
93145
precedencet precedence)
@@ -112,10 +164,18 @@ expr2smvt::resultt expr2smvt::convert_binary(
112164

113165
auto op_rec = convert_rec(*it);
114166

115-
if(precedence > op_rec.p)
167+
// clang-format off
168+
bool use_parentheses =
169+
src.id() == it->id() ? false
170+
: precedence >= op_rec.p;
171+
// clang-format on
172+
173+
if(use_parentheses)
116174
dest += '(';
175+
117176
dest += op_rec.s;
118-
if(precedence > op_rec.p)
177+
178+
if(use_parentheses)
119179
dest += ')';
120180
}
121181

@@ -449,15 +509,10 @@ Function: expr2smvt::convert_rec
449509
expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
450510
{
451511
if(src.id()==ID_plus)
452-
return convert_binary(src, "+", precedencet::PLUS);
512+
return convert_binary_associative(src, "+", precedencet::PLUS);
453513

454514
else if(src.id()==ID_minus)
455-
{
456-
if(src.operands().size()<2)
457-
return convert_norep(src);
458-
else
459-
return convert_binary(src, "-", precedencet::PLUS);
460-
}
515+
return convert_binary_associative(src, "-", precedencet::PLUS);
461516

462517
else if(src.id()==ID_unary_minus)
463518
{
@@ -470,57 +525,65 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
470525
else if(src.id()==ID_index)
471526
return convert_index(to_index_expr(src), precedencet::INDEX);
472527

473-
else if(src.id()==ID_mult || src.id()==ID_div)
474-
return convert_binary(src, src.id_string(), precedencet::MULT);
528+
else if(src.id() == ID_mult)
529+
return convert_binary_associative(src, src.id_string(), precedencet::MULT);
530+
531+
else if(src.id() == ID_div)
532+
return convert_binary(to_div_expr(src), src.id_string(), precedencet::MULT);
475533

476534
else if(src.id() == ID_mod)
477-
return convert_binary(src, src.id_string(), precedencet::MULT);
535+
return convert_binary(to_mod_expr(src), src.id_string(), precedencet::MULT);
478536

479537
else if(src.id() == ID_smv_setin)
480-
return convert_binary(src, "in", precedencet::IN);
538+
return convert_binary(to_binary_expr(src), "in", precedencet::IN);
481539

482540
else if(src.id() == ID_smv_setnotin)
483-
return convert_binary(src, "notin", precedencet::IN);
541+
return convert_binary(to_binary_expr(src), "notin", precedencet::IN);
484542

485543
else if(src.id() == ID_smv_union)
486-
return convert_binary(src, "union", precedencet::UNION);
544+
return convert_binary(to_binary_expr(src), "union", precedencet::UNION);
487545

488546
else if(src.id()==ID_lt || src.id()==ID_gt ||
489547
src.id()==ID_le || src.id()==ID_ge)
490-
return convert_binary(src, src.id_string(), precedencet::REL);
548+
return convert_binary(
549+
to_binary_expr(src), src.id_string(), precedencet::REL);
491550

492551
else if(src.id()==ID_equal)
493552
{
494-
if(src.get_bool(ID_C_smv_iff))
495-
return convert_binary(src, "<->", precedencet::IFF);
553+
auto &equal_expr = to_equal_expr(src);
554+
555+
if(equal_expr.get_bool(ID_C_smv_iff))
556+
return convert_binary(equal_expr, "<->", precedencet::IFF);
496557
else
497-
return convert_binary(src, "=", precedencet::REL);
558+
return convert_binary(equal_expr, "=", precedencet::REL);
498559
}
499560

500561
else if(src.id()==ID_notequal)
501-
return convert_binary(src, "!=", precedencet::REL);
562+
return convert_binary(to_notequal_expr(src), "!=", precedencet::REL);
502563

503564
else if(src.id()==ID_not)
504565
return convert_unary(to_not_expr(src), "!", precedencet::NOT);
505566

506567
else if(src.id() == ID_and || src.id() == ID_bitand)
507-
return convert_binary(src, "&", precedencet::AND);
568+
return convert_binary_associative(src, "&", precedencet::AND);
508569

509570
else if(src.id() == ID_or || src.id() == ID_bitor)
510-
return convert_binary(src, "|", precedencet::OR);
571+
return convert_binary_associative(src, "|", precedencet::OR);
511572

512573
else if(src.id() == ID_implies || src.id() == ID_smv_bitimplies)
513-
return convert_binary(src, "->", precedencet::IMPLIES);
574+
return convert_binary(to_binary_expr(src), "->", precedencet::IMPLIES);
514575

515576
else if(src.id() == ID_xor || src.id() == ID_bitxor)
516-
return convert_binary(src, "xor", precedencet::OR);
577+
return convert_binary_associative(src, "xor", precedencet::OR);
517578

518579
else if(src.id() == ID_xnor || src.id() == ID_bitxnor)
519580
{
581+
auto &binary_expr = to_binary_expr(src);
582+
520583
if(src.get_bool(ID_C_smv_iff))
521-
return convert_binary(src, "<->", precedencet::IFF);
584+
return convert_binary(binary_expr, "<->", precedencet::IFF);
522585
else
523-
return convert_binary(src, "xnor", precedencet::OR);
586+
return convert_binary(binary_expr, "xnor", precedencet::OR);
524587
}
525588

526589
else if(
@@ -623,7 +686,8 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
623686

624687
else if(src.id() == ID_concatenation)
625688
{
626-
return convert_binary(to_binary_expr(src), "::", precedencet::CONCAT);
689+
return convert_binary_associative(
690+
to_binary_expr(src), "::", precedencet::CONCAT);
627691
}
628692

629693
else if(src.id() == ID_shl)

‎src/smvlang/expr2smv_class.h

+9-2
Original file line numberDiff line numberDiff line change
@@ -87,8 +87,15 @@ class expr2smvt
8787

8888
resultt convert_nondet_choice(const exprt &);
8989

90-
resultt
91-
convert_binary(const exprt &src, const std::string &symbol, precedencet);
90+
resultt convert_binary(
91+
const binary_exprt &src,
92+
const std::string &symbol,
93+
precedencet);
94+
95+
resultt convert_binary_associative(
96+
const exprt &src,
97+
const std::string &symbol,
98+
precedencet);
9299

93100
resultt convert_rtctl(
94101
const ternary_exprt &src,

‎unit/Makefile

+4-2
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,8 @@
44
SRC = unit_tests.cpp
55

66
# Test source files
7-
SRC += temporal-logic/nnf.cpp \
7+
SRC += smvlang/expr2smv.cpp \
8+
temporal-logic/nnf.cpp \
89
# Empty last line
910

1011
INCLUDES= -I ../src/ -I . -I $(CPROVER_DIR)/unit -I $(CPROVER_DIR)/src
@@ -16,7 +17,8 @@ include $(CPROVER_DIR)/src/common
1617

1718
CXXFLAGS += -D'LOCAL_IREP_IDS=<hw_cbmc_irep_ids.h>'
1819

19-
OBJ += ../src/temporal-logic/temporal-logic$(LIBEXT)
20+
OBJ += ../src/smvlang/smvlang$(LIBEXT) \
21+
../src/temporal-logic/temporal-logic$(LIBEXT)
2022

2123
cprover.dir:
2224
$(MAKE) $(MAKEARGS) -C ../src

‎unit/smvlang/expr2smv.cpp

+38
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
/*******************************************************************\
2+
3+
Module: expr2smv Unit Tests
4+
5+
Author: Daniel Kroening, Amazon, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <util/arith_tools.h>
10+
#include <util/mathematical_types.h>
11+
#include <util/namespace.h>
12+
#include <util/std_expr.h>
13+
#include <util/symbol_table.h>
14+
15+
#include <smvlang/expr2smv.h>
16+
#include <testing-utils/use_catch.h>
17+
18+
SCENARIO("Generating SMV expression strings")
19+
{
20+
const symbol_tablet symbol_table;
21+
const namespacet empty_ns{symbol_table};
22+
23+
GIVEN("An expression with non-associative operators")
24+
{
25+
auto t = integer_typet{};
26+
auto n = [t](mp_integer i) { return from_integer(i, t); };
27+
auto expr = div_exprt{n(3), div_exprt{n(4), n(2)}};
28+
REQUIRE(expr2smv(expr, empty_ns) == "3 / (4 / 2)");
29+
}
30+
31+
GIVEN("An expression with associative operators")
32+
{
33+
auto t = integer_typet{};
34+
auto n = [t](mp_integer i) { return from_integer(i, t); };
35+
auto expr = plus_exprt{n(3), plus_exprt{n(4), n(2)}};
36+
REQUIRE(expr2smv(expr, empty_ns) == "3 + 4 + 2");
37+
}
38+
}

0 commit comments

Comments
 (0)