diff --git a/regression/ebmc/smv-word-level/verilog1.desc b/regression/ebmc/smv-word-level/verilog1.desc index d4dfef295..2c9a6ebca 100644 --- a/regression/ebmc/smv-word-level/verilog1.desc +++ b/regression/ebmc/smv-word-level/verilog1.desc @@ -4,7 +4,7 @@ verilog1.sv ^MODULE main$ ^VAR x : unsigned word\[32\];$ ^INIT main\.x = 0ud32_0$ -^INVAR Verilog::main\.x_aux0 = main\.x \+ 0ud32_1$ +^INVAR Verilog::main\.x_aux0 = main\.x \+ unsigned\(0sd32_1\)$ ^TRANS next\(main\.x\) = Verilog::main\.x_aux0$ ^LTLSPEC F main\.x = unsigned\(0sd32_10\)$ ^EXIT=0$ diff --git a/regression/verilog/assignments/assignment-with-function-call1.sv b/regression/verilog/assignments/assignment-with-function-call1.sv index 5dd9a5857..2f8f431d9 100644 --- a/regression/verilog/assignments/assignment-with-function-call1.sv +++ b/regression/verilog/assignments/assignment-with-function-call1.sv @@ -10,8 +10,8 @@ module top(input [7:0] a, input [7:0] b); wire [7:0] sum_a_b = fn(a, b), sum_1_2 = fn(1, 2), sum_2_3 = fn(2, 3); - - assert property (sum_a_b==a[2:0]+b[2:0]); + + assert property (sum_a_b[2:0]==a[2:0]+b[2:0]); assert property (sum_1_2==3); diff --git a/regression/verilog/expressions/equality1.desc b/regression/verilog/expressions/equality1.desc index e9fed273e..2418f3ee1 100644 --- a/regression/verilog/expressions/equality1.desc +++ b/regression/verilog/expressions/equality1.desc @@ -10,7 +10,7 @@ equality1.v ^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED .*$ ^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED .*$ ^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED .*$ -^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED .*$ +^\[.*\] always 1'sb1 == 2'sb11 === 1: PROVED .*$ ^\[.*\] always 1\.1 == 1\.1 == 1: PROVED .*$ ^\[.*\] always 1\.1 == 1 == 0: PROVED .*$ ^EXIT=0$ diff --git a/regression/verilog/expressions/equality2.desc b/regression/verilog/expressions/equality2.desc index f70993dbe..179c844c4 100644 --- a/regression/verilog/expressions/equality2.desc +++ b/regression/verilog/expressions/equality2.desc @@ -12,7 +12,7 @@ equality2.v ^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED .*$ ^\[.*\] always 1 === 1 == 1: PROVED .*$ ^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED .*$ -^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED .*$ +^\[.*\] always 3'sb111 === 2'sb11 == 1: PROVED .*$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/shl4.desc b/regression/verilog/expressions/shl4.desc index c467a78ce..7b1140269 100644 --- a/regression/verilog/expressions/shl4.desc +++ b/regression/verilog/expressions/shl4.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE broken-smt-backend shl4.sv --bound 0 ^EXIT=0$ @@ -6,4 +6,3 @@ shl4.sv -- ^warning: ignoring -- -This gives the wrong answer. diff --git a/regression/verilog/expressions/wildcard_equality1.desc b/regression/verilog/expressions/wildcard_equality1.desc index 302a4fdfc..e0457f8b1 100644 --- a/regression/verilog/expressions/wildcard_equality1.desc +++ b/regression/verilog/expressions/wildcard_equality1.desc @@ -10,7 +10,7 @@ wildcard_equality1.sv ^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED .*$ ^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED .*$ ^\[main\.property09\] always 1'sb1 ==\? 2'b11 === 0: PROVED .*$ -^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED .*$ +^\[main\.property10\] always 1'sb1 ==\? 2'sb11 === 1: PROVED .*$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/past6.desc b/regression/verilog/system-functions/past6.desc index 79d8dc66c..3432b717a 100644 --- a/regression/verilog/system-functions/past6.desc +++ b/regression/verilog/system-functions/past6.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend past6.sv ^EXIT=10$ diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 1c9d3f30e..9df8862dd 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -222,6 +222,39 @@ void verilog_typecheck_exprt::propagate_type( /*******************************************************************\ +Function: zero_extend + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static exprt zero_extend(const exprt &expr, const typet &type) +{ + auto old_width = expr.type().id() == ID_bool ? 1 + : expr.type().id() == ID_integer + ? 32 + : to_bitvector_type(expr.type()).get_width(); + + // first make unsigned + typet tmp_type; + + if(type.id() == ID_unsignedbv) + tmp_type = unsignedbv_typet{old_width}; + else if(type.id() == ID_verilog_unsignedbv) + tmp_type = verilog_unsignedbv_typet{old_width}; + else + PRECONDITION(false); + + return typecast_exprt::conditional_cast( + typecast_exprt::conditional_cast(expr, tmp_type), type); +} + +/*******************************************************************\ + Function: verilog_typecheck_exprt::downwards_type_progatation Inputs: @@ -241,95 +274,69 @@ void verilog_typecheck_exprt::downwards_type_propagation( // Any context-determined operand of an operator shall be the // same type and size as the result of the operator. - // Exceptions: - // * result type real -- just cast - // * relational operators are always 1 bit unsigned + // As an exception, if the result type is real, the operands + // are just casted. if(expr.type() == type) return; - vtypet vt_from = vtypet(expr.type()); - vtypet vt_to = vtypet(type); - - if(!vt_from.is_other() && !vt_to.is_other() && expr.has_operands()) + if(type.id() == ID_verilog_real || type.id() == ID_verilog_shortreal) { - // arithmetic - - if( - expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult || - expr.id() == ID_div || expr.id() == ID_unary_minus || - expr.id() == ID_unary_plus) - { - if(type.id() != ID_bool) - { - Forall_operands(it, expr) - propagate_type(*it, type); - - expr.type() = type; - - return; - } - } - else if( - expr.id() == ID_bitand || expr.id() == ID_bitor || - expr.id() == ID_bitnand || expr.id() == ID_bitnor || - expr.id() == ID_bitxor || expr.id() == ID_bitxnor || - expr.id() == ID_bitnot) - { - Forall_operands(it, expr) - propagate_type(*it, type); - - expr.type() = type; - - if(type.id() == ID_bool) - { - if(expr.id() == ID_bitand) - expr.id(ID_and); - else if(expr.id() == ID_bitor) - expr.id(ID_or); - else if(expr.id() == ID_bitnand) - expr.id(ID_nand); - else if(expr.id() == ID_bitnor) - expr.id(ID_nor); - else if(expr.id() == ID_bitxor) - expr.id(ID_xor); - else if(expr.id() == ID_bitxnor) - expr.id(ID_xnor); - else if(expr.id() == ID_bitnot) - expr.id(ID_not); - } - - return; - } - else if(expr.id() == ID_if) - { - if(expr.operands().size() == 3) - { - propagate_type(to_if_expr(expr).true_case(), type); - propagate_type(to_if_expr(expr).false_case(), type); - - expr.type() = type; - return; - } - } - else if(expr.id() == ID_shl) // does not work with shr - { - // does not work with boolean - if(type.id() != ID_bool) - { - if(expr.operands().size() == 2) - { - propagate_type(to_binary_expr(expr).op0(), type); - // not applicable to second operand + expr = typecast_exprt{expr, type}; + return; + } - expr.type() = type; - return; - } - } - } + // expressions with context-determined width, following + // 1800-2017 Table 11-21 + if( + expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult || + expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitand || + expr.id() == ID_bitor || expr.id() == ID_bitxor || + expr.id() == ID_bitxnor || expr.id() == ID_unary_plus || + expr.id() == ID_unary_minus || expr.id() == ID_bitnot) + { + // All operands are context-determined. + for(auto &op : expr.operands()) + downwards_type_propagation(op, type); + expr.type() = type; + return; + } + else if( + expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr || + expr.id() == ID_power) + { + // The LHS is context-determined, the RHS is self-determined + auto &binary_expr = to_binary_expr(expr); + downwards_type_propagation(binary_expr.lhs(), type); + expr.type() = type; + return; + } + else if(expr.id() == ID_if) + { + // The first operand is self-determined, the others are context-determined + auto &if_expr = to_if_expr(expr); + downwards_type_propagation(if_expr.op1(), type); + downwards_type_propagation(if_expr.op2(), type); + expr.type() = type; + return; } - implicit_typecast(expr, type); + // Just cast the expression, leave any operands as they are. + if( + (expr.type().id() == ID_signedbv || + expr.type().id() == ID_verilog_signedbv) && + (type.id() == ID_unsignedbv || type.id() == ID_verilog_unsignedbv) && + get_width(expr.type()) < get_width(type)) + { + // "If the operand shall be extended, then it shall be sign-extended only + // if the propagated type is signed." + // A typecast from signed to a larger unsigned would sign extend. + expr = zero_extend(expr, type); + } + else + { + expr = typecast_exprt{expr, type}; + } } /*******************************************************************\ @@ -2535,39 +2542,6 @@ void verilog_typecheck_exprt::tc_binary_expr( /*******************************************************************\ -Function: zero_extend - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -static exprt zero_extend(const exprt &expr, const typet &type) -{ - auto old_width = expr.type().id() == ID_bool ? 1 - : expr.type().id() == ID_integer - ? 32 - : to_bitvector_type(expr.type()).get_width(); - - // first make unsigned - typet tmp_type; - - if(type.id() == ID_unsignedbv) - tmp_type = unsignedbv_typet{old_width}; - else if(type.id() == ID_verilog_unsignedbv) - tmp_type = verilog_unsignedbv_typet{old_width}; - else - PRECONDITION(false); - - return typecast_exprt::conditional_cast( - typecast_exprt::conditional_cast(expr, tmp_type), type); -} - -/*******************************************************************\ - Function: verilog_typecheck_exprt::convert_relation Inputs: @@ -2580,43 +2554,11 @@ Function: verilog_typecheck_exprt::convert_relation void verilog_typecheck_exprt::convert_relation(binary_exprt &expr) { - auto &lhs = expr.lhs(); - auto &rhs = expr.rhs(); - - convert_expr(lhs); - convert_expr(rhs); - - union_decay(lhs); - union_decay(rhs); - - // Relations are special-cased in 1800-2017 11.8.2. - const typet new_type = - max_type(enum_decay(lhs.type()), enum_decay(rhs.type())); - - if(new_type.is_nil()) - { - throw errort().with_location(expr.source_location()) - << "expected operands of compatible type but got:\n" - << " " << to_string(lhs.type()) << '\n' - << " " << to_string(rhs.type()); - } + convert_expr(expr.lhs()); + convert_expr(expr.rhs()); - // If both operands are signed, both are sign-extended to the max width. - // Otherwise, both are zero-extended to the max width. - // In particular, signed operands are then _not_ sign extended, - // which a typecast would do. - if(new_type.id() == ID_verilog_unsignedbv || new_type.id() == ID_unsignedbv) - { - // zero extend both operands - lhs = zero_extend(lhs, new_type); - rhs = zero_extend(rhs, new_type); - } - else - { - // convert - implicit_typecast(lhs, new_type); - implicit_typecast(rhs, new_type); - } + // determine the max of the operand types and propagate it downwards + tc_binary_expr(expr); } /*******************************************************************\