From 51b70df5636c74a78520710ce8148c8495193f08 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 18 Sep 2024 21:58:33 -0400 Subject: [PATCH] SMV: use ID_smv_iff for <-> This changes the SMV front-end to use ID_smv_iff for <->. --- regression/ebmc/smv/smv_iff1.desc | 7 +++++++ regression/ebmc/smv/smv_iff1.smv | 9 +++++++++ regression/ebmc/smv/smv_iff2.desc | 7 +++++++ regression/ebmc/smv/smv_iff2.smv | 14 ++++++++++++++ src/ebmc/bdd_engine.cpp | 11 ++++++++++- src/hw_cbmc_irep_ids.h | 4 +++- src/smvlang/expr2smv.cpp | 10 ++++++---- src/smvlang/parser.y | 2 +- src/smvlang/smv_typecheck.cpp | 13 +++++++++---- src/verilog/expr2verilog.cpp | 2 +- src/verilog/parser.y | 2 +- src/verilog/verilog_typecheck_expr.cpp | 2 +- 12 files changed, 69 insertions(+), 14 deletions(-) create mode 100644 regression/ebmc/smv/smv_iff1.desc create mode 100644 regression/ebmc/smv/smv_iff1.smv create mode 100644 regression/ebmc/smv/smv_iff2.desc create mode 100644 regression/ebmc/smv/smv_iff2.smv diff --git a/regression/ebmc/smv/smv_iff1.desc b/regression/ebmc/smv/smv_iff1.desc new file mode 100644 index 000000000..61fb9f359 --- /dev/null +++ b/regression/ebmc/smv/smv_iff1.desc @@ -0,0 +1,7 @@ +CORE +smv_iff1.smv + +^file .* line 9: Expected expression of type `boolean', but got expression `x', which is of type `0..10'$ +^EXIT=2$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/smv/smv_iff1.smv b/regression/ebmc/smv/smv_iff1.smv new file mode 100644 index 000000000..79210f40b --- /dev/null +++ b/regression/ebmc/smv/smv_iff1.smv @@ -0,0 +1,9 @@ +MODULE main + +VAR x : 0..10; + +ASSIGN init(x) := 1; + next(x) := x; + +-- type error: lhs is not Boolean +SPEC x <-> (x != 0) diff --git a/regression/ebmc/smv/smv_iff2.desc b/regression/ebmc/smv/smv_iff2.desc new file mode 100644 index 000000000..8f0eb76f7 --- /dev/null +++ b/regression/ebmc/smv/smv_iff2.desc @@ -0,0 +1,7 @@ +CORE +smv_iff2.smv +--bdd +^\[.*\] \(AG x != 5\) <-> \(x != 5 & AX AG x != 5\): PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc/smv/smv_iff2.smv b/regression/ebmc/smv/smv_iff2.smv new file mode 100644 index 000000000..38c0b265e --- /dev/null +++ b/regression/ebmc/smv/smv_iff2.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR x : 0..10; + +ASSIGN + init(x) := 1; + + next(x) := + case + x>=3 : 3; + TRUE: x+1; + esac; + +SPEC AG x != 5 <-> (x != 5 & AX AG x != 5) diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index 6f4578850..6fa0a05a6 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -673,6 +673,12 @@ bdd_enginet::BDD bdd_enginet::CTL(const exprt &expr) result = result | CTL(op); return result; } + else if( + expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool) + { + return ( + !(CTL(to_binary_expr(expr).lhs())) ^ CTL(to_binary_expr(expr).rhs())); + } else if(expr.id() == ID_EX) { return EX(CTL(to_EX_expr(expr).op())); @@ -891,7 +897,10 @@ void bdd_enginet::get_atomic_propositions(const exprt &expr) { if( expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not || - expr.id() == ID_implies || is_temporal_operator(expr)) + expr.id() == ID_implies || + (expr.id() == ID_equal && + to_equal_expr(expr).lhs().type().id() == ID_bool) || + is_temporal_operator(expr)) { for(const auto & op : expr.operands()) if(op.type().id() == ID_bool) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 18937b6cb..f60876b32 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -15,6 +15,8 @@ IREP_ID_ONE(F) IREP_ID_ONE(E) IREP_ID_ONE(G) IREP_ID_ONE(X) +IREP_ID_ONE(smv_iff) +IREP_ID_TWO(C_smv_iff, "#smv_iff") IREP_ID_ONE(sva_accept_on) IREP_ID_ONE(sva_reject_on) IREP_ID_ONE(sva_sync_accept_on) @@ -215,7 +217,7 @@ IREP_ID_ONE(verilog_ref) IREP_ID_ONE(verilog_reg) IREP_ID_ONE(verilog_integer) IREP_ID_ONE(verilog_time) -IREP_ID_ONE(iff) +IREP_ID_ONE(verilog_iff) IREP_ID_ONE(offset) IREP_ID_ONE(xnor) IREP_ID_ONE(specify) diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index f6efb7443..af9ce2c33 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -449,7 +449,12 @@ bool expr2smvt::convert( return convert_binary(src, dest, src.id_string(), precedence=11); else if(src.id()==ID_equal) - return convert_binary(src, dest, "=", precedence=11); + { + if(src.get_bool(ID_C_smv_iff)) + return convert_binary(src, dest, "<->", precedence = 16); + else + return convert_binary(src, dest, "=", precedence = 11); + } else if(src.id()==ID_notequal) return convert_binary(src, dest, "!=", precedence=11); @@ -466,9 +471,6 @@ bool expr2smvt::convert( else if(src.id()==ID_implies) return convert_binary(src, dest, "->", precedence=2); - else if(src.id()==ID_iff) - return convert_binary(src, dest, "<->", precedence=3); - else if( src.id() == ID_AG || src.id() == ID_EG || src.id() == ID_AF || src.id() == ID_EF || src.id() == ID_AX || src.id() == ID_EX || diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index b2668b859..b67b79728 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -455,7 +455,7 @@ term : variable_name | term DIVIDE_Token term { binary_arith($$, $1, ID_div, $3); } | term PLUS_Token term { binary_arith($$, $1, ID_plus, $3); } | term MINUS_Token term { binary_arith($$, $1, ID_minus, $3); } - | term EQUIV_Token term { binary($$, $1, ID_equal, $3, bool_typet{}); } + | term EQUIV_Token term { binary($$, $1, ID_smv_iff, $3, bool_typet{}); } | term IMPLIES_Token term { binary($$, $1, ID_implies, $3, bool_typet{}); } | term XOR_Token term { j_binary($$, $1, ID_xor, $3, bool_typet{}); } | term OR_Token term { j_binary($$, $1, ID_or, $3, bool_typet{}); } diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 30933570f..fec614cfb 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -681,12 +681,17 @@ void smv_typecheckt::typecheck( } } } - else if(expr.id()==ID_and || - expr.id()==ID_or || - expr.id()==ID_xor || - expr.id()==ID_not) + else if( + expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_xor || + expr.id() == ID_not) + { + typecheck_op(expr, bool_typet(), mode); + } + else if(expr.id() == ID_smv_iff) { typecheck_op(expr, bool_typet(), mode); + expr.set(ID_C_smv_iff, true); + expr.id(ID_equal); } else if(expr.id()==ID_nondet_symbol) { diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index d57afb445..7971ebf56 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1337,7 +1337,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) return convert_binary( to_multi_ary_expr(src), "->", precedence = verilog_precedencet::IMPLIES); - else if(src.id()==ID_iff) + else if(src.id() == ID_verilog_iff) return convert_binary( to_multi_ary_expr(src), "<->", precedence = verilog_precedencet::IMPLIES); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index b2c83e378..8b0154fd8 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -3534,7 +3534,7 @@ expression: | expression "->" expression { init($$, ID_implies); mto($$, $1); mto($$, $3); } | expression "<->" expression - { init($$, ID_iff); mto($$, $1); mto($$, $3); } + { init($$, ID_verilog_iff); mto($$, $1); mto($$, $3); } | expression TOK_PLUS expression { init($$, ID_plus); mto($$, $1); mto($$, $3); } | expression TOK_MINUS expression diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index a56d2443b..47a75c902 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2644,7 +2644,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) else if(expr.id()==ID_replication) return convert_replication_expr(to_replication_expr(expr)); else if( - expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_iff || + expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_verilog_iff || expr.id() == ID_implies) { Forall_operands(it, expr)