From 090d419ccb202ff582217bdb02a46b190128e54a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 17 Dec 2024 09:30:52 -0800 Subject: [PATCH 1/2] Bump CBMC dependency --- lib/cbmc | 2 +- regression/ebmc/range_type/range_type1.desc | 2 +- regression/ebmc/range_type/range_type4.desc | 2 +- regression/ebmc/traces/disjunction1.desc | 2 +- regression/smv/CTL/smv_ctlspec_F1.desc | 2 +- regression/smv/CTL/smv_ctlspec_G1.desc | 2 +- regression/smv/LTL/smv_ltlspec6.desc | 2 +- regression/smv/LTL/smv_ltlspec_F1.desc | 2 +- regression/smv/LTL/smv_ltlspec_F2.desc | 2 +- regression/smv/LTL/smv_ltlspec_F3.desc | 2 +- regression/smv/LTL/smv_ltlspec_G1.desc | 2 +- regression/smv/LTL/smv_ltlspec_G2.desc | 2 +- regression/smv/LTL/smv_ltlspec_G3.desc | 2 +- regression/smv/LTL/smv_ltlspec_R1.desc | 2 +- regression/smv/LTL/smv_ltlspec_R3.desc | 2 +- regression/smv/LTL/smv_ltlspec_R4.desc | 2 +- regression/smv/LTL/smv_ltlspec_U1.desc | 2 +- regression/smv/LTL/smv_ltlspec_U2.desc | 2 +- regression/smv/expressions/smv_if1.desc | 2 +- .../verilog/assignments/assignment-to-concatenation1.desc | 2 +- regression/verilog/assignments/assignment-to-index1.desc | 2 +- regression/verilog/generate/generate-for2.desc | 2 +- regression/verilog/generate/generate-reg1.desc | 2 +- regression/verilog/generate1/test.desc | 2 +- regression/verilog/multiple_assign1/test.desc | 2 +- regression/verilog/part-select/indexed-part-select1.desc | 2 +- regression/verilog/primitive_gates/nand1.desc | 2 +- regression/verilog/primitive_gates/xnor3.desc | 2 +- regression/verilog/system-functions/low1.desc | 2 +- src/ebmc/ebmc_parse_options.cpp | 6 ++---- src/hw_cbmc_irep_ids.h | 1 - src/verilog/verilog_synthesis.cpp | 6 ++---- 32 files changed, 33 insertions(+), 38 deletions(-) diff --git a/lib/cbmc b/lib/cbmc index c902db34b..fb2847509 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit c902db34beb113815f151c4d1f635e745ac79c0c +Subproject commit fb284750934f5830501990d54c1d8118c7af0d3d diff --git a/regression/ebmc/range_type/range_type1.desc b/regression/ebmc/range_type/range_type1.desc index 6a72be6c8..cd48ef65c 100644 --- a/regression/ebmc/range_type/range_type1.desc +++ b/regression/ebmc/range_type/range_type1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE range_type1.smv --bound 10 ^EXIT=0$ diff --git a/regression/ebmc/range_type/range_type4.desc b/regression/ebmc/range_type/range_type4.desc index 8c4b05d8f..c36e4105c 100644 --- a/regression/ebmc/range_type/range_type4.desc +++ b/regression/ebmc/range_type/range_type4.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE range_type4.smv --bound 10 ^EXIT=0$ diff --git a/regression/ebmc/traces/disjunction1.desc b/regression/ebmc/traces/disjunction1.desc index c5b16109f..979937e30 100644 --- a/regression/ebmc/traces/disjunction1.desc +++ b/regression/ebmc/traces/disjunction1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE disjunction1.smv --bound 20 --numbered-trace ^\[spec1\] G \(X FALSE \| X X FALSE\): REFUTED$ diff --git a/regression/smv/CTL/smv_ctlspec_F1.desc b/regression/smv/CTL/smv_ctlspec_F1.desc index 3fac6aacc..91236eccb 100644 --- a/regression/smv/CTL/smv_ctlspec_F1.desc +++ b/regression/smv/CTL/smv_ctlspec_F1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ctlspec_F1.smv --bound 10 ^\[.*\] AF x = 0: REFUTED$ diff --git a/regression/smv/CTL/smv_ctlspec_G1.desc b/regression/smv/CTL/smv_ctlspec_G1.desc index 291451aeb..e2604b804 100644 --- a/regression/smv/CTL/smv_ctlspec_G1.desc +++ b/regression/smv/CTL/smv_ctlspec_G1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ctlspec_G1.smv --bound 10 ^\[.*\] AG x != 5: PROVED up to bound 10$ diff --git a/regression/smv/LTL/smv_ltlspec6.desc b/regression/smv/LTL/smv_ltlspec6.desc index cbb97eb47..b2736a00d 100644 --- a/regression/smv/LTL/smv_ltlspec6.desc +++ b/regression/smv/LTL/smv_ltlspec6.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec6.smv ^EXIT=0$ diff --git a/regression/smv/LTL/smv_ltlspec_F1.desc b/regression/smv/LTL/smv_ltlspec_F1.desc index e716671d2..6b072e0a7 100644 --- a/regression/smv/LTL/smv_ltlspec_F1.desc +++ b/regression/smv/LTL/smv_ltlspec_F1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_F1.smv --bound 10 ^EXIT=10$ diff --git a/regression/smv/LTL/smv_ltlspec_F2.desc b/regression/smv/LTL/smv_ltlspec_F2.desc index 7b672c256..8fe3683c5 100644 --- a/regression/smv/LTL/smv_ltlspec_F2.desc +++ b/regression/smv/LTL/smv_ltlspec_F2.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_F2.smv --bound 10 ^EXIT=10$ diff --git a/regression/smv/LTL/smv_ltlspec_F3.desc b/regression/smv/LTL/smv_ltlspec_F3.desc index d4ff52613..db908e9f8 100644 --- a/regression/smv/LTL/smv_ltlspec_F3.desc +++ b/regression/smv/LTL/smv_ltlspec_F3.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_F3.smv --bound 10 --numbered-trace ^\[.*\] F x = 0: REFUTED$ diff --git a/regression/smv/LTL/smv_ltlspec_G1.desc b/regression/smv/LTL/smv_ltlspec_G1.desc index f36e383c8..5946bb2a5 100644 --- a/regression/smv/LTL/smv_ltlspec_G1.desc +++ b/regression/smv/LTL/smv_ltlspec_G1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_G1.smv --bound 10 ^EXIT=10$ diff --git a/regression/smv/LTL/smv_ltlspec_G2.desc b/regression/smv/LTL/smv_ltlspec_G2.desc index e32cce870..cc411baaa 100644 --- a/regression/smv/LTL/smv_ltlspec_G2.desc +++ b/regression/smv/LTL/smv_ltlspec_G2.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_G2.smv --bound 10 ^EXIT=10$ diff --git a/regression/smv/LTL/smv_ltlspec_G3.desc b/regression/smv/LTL/smv_ltlspec_G3.desc index 71e3a27a4..5d4a558a6 100644 --- a/regression/smv/LTL/smv_ltlspec_G3.desc +++ b/regression/smv/LTL/smv_ltlspec_G3.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_G3.smv --bound 10 --numbered-trace ^\[.*\] G X x != 3: REFUTED$ diff --git a/regression/smv/LTL/smv_ltlspec_R1.desc b/regression/smv/LTL/smv_ltlspec_R1.desc index 4d84bdbfc..3233a406a 100644 --- a/regression/smv/LTL/smv_ltlspec_R1.desc +++ b/regression/smv/LTL/smv_ltlspec_R1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_R1.smv --bound 10 ^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$ diff --git a/regression/smv/LTL/smv_ltlspec_R3.desc b/regression/smv/LTL/smv_ltlspec_R3.desc index 7b5d9356e..55688211b 100644 --- a/regression/smv/LTL/smv_ltlspec_R3.desc +++ b/regression/smv/LTL/smv_ltlspec_R3.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_R3.smv --bound 1 ^\[.*\] FALSE R x != 3: PROVED up to bound 1$ diff --git a/regression/smv/LTL/smv_ltlspec_R4.desc b/regression/smv/LTL/smv_ltlspec_R4.desc index fe268f524..7671d6989 100644 --- a/regression/smv/LTL/smv_ltlspec_R4.desc +++ b/regression/smv/LTL/smv_ltlspec_R4.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_R4.smv --bound 10 ^\[.*\] FALSE R x != 0: PROVED up to bound 10$ diff --git a/regression/smv/LTL/smv_ltlspec_U1.desc b/regression/smv/LTL/smv_ltlspec_U1.desc index febf0d1f4..e59b642c5 100644 --- a/regression/smv/LTL/smv_ltlspec_U1.desc +++ b/regression/smv/LTL/smv_ltlspec_U1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_U1.smv --bound 3 \[.*\] TRUE U x = 3: PROVED up to bound 3$ diff --git a/regression/smv/LTL/smv_ltlspec_U2.desc b/regression/smv/LTL/smv_ltlspec_U2.desc index ec6a58f8d..09c3f8db0 100644 --- a/regression/smv/LTL/smv_ltlspec_U2.desc +++ b/regression/smv/LTL/smv_ltlspec_U2.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_ltlspec_U2.smv --bound 10 --numbered-trace ^\[.*\] TRUE U x = 0: REFUTED$ diff --git a/regression/smv/expressions/smv_if1.desc b/regression/smv/expressions/smv_if1.desc index 3ee995e40..7bc5966ae 100644 --- a/regression/smv/expressions/smv_if1.desc +++ b/regression/smv/expressions/smv_if1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE smv_if1.smv ^EXIT=0$ diff --git a/regression/verilog/assignments/assignment-to-concatenation1.desc b/regression/verilog/assignments/assignment-to-concatenation1.desc index 673825e1d..7a8281593 100644 --- a/regression/verilog/assignments/assignment-to-concatenation1.desc +++ b/regression/verilog/assignments/assignment-to-concatenation1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE assignment-to-concatenation1.v --bound 1 ^EXIT=0$ diff --git a/regression/verilog/assignments/assignment-to-index1.desc b/regression/verilog/assignments/assignment-to-index1.desc index a1f0805c5..37d4c7250 100644 --- a/regression/verilog/assignments/assignment-to-index1.desc +++ b/regression/verilog/assignments/assignment-to-index1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE assignment-to-index1.v --bound 1 ^EXIT=0$ diff --git a/regression/verilog/generate/generate-for2.desc b/regression/verilog/generate/generate-for2.desc index ec4829241..168a17e6e 100644 --- a/regression/verilog/generate/generate-for2.desc +++ b/regression/verilog/generate/generate-for2.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE generate-for2.v --bound 0 ^EXIT=0$ diff --git a/regression/verilog/generate/generate-reg1.desc b/regression/verilog/generate/generate-reg1.desc index 01c703bc9..60a3c80a2 100644 --- a/regression/verilog/generate/generate-reg1.desc +++ b/regression/verilog/generate/generate-reg1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE generate-reg1.v --module main --bound 0 ^EXIT=0$ diff --git a/regression/verilog/generate1/test.desc b/regression/verilog/generate1/test.desc index 415cc5c10..6a3d0fa20 100644 --- a/regression/verilog/generate1/test.desc +++ b/regression/verilog/generate1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.v --module main --bound 1 ^EXIT=0$ diff --git a/regression/verilog/multiple_assign1/test.desc b/regression/verilog/multiple_assign1/test.desc index 415cc5c10..6a3d0fa20 100644 --- a/regression/verilog/multiple_assign1/test.desc +++ b/regression/verilog/multiple_assign1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.v --module main --bound 1 ^EXIT=0$ diff --git a/regression/verilog/part-select/indexed-part-select1.desc b/regression/verilog/part-select/indexed-part-select1.desc index 39181c2be..5990bdc0d 100644 --- a/regression/verilog/part-select/indexed-part-select1.desc +++ b/regression/verilog/part-select/indexed-part-select1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE indexed-part-select1.sv --bound 0 ^EXIT=0$ diff --git a/regression/verilog/primitive_gates/nand1.desc b/regression/verilog/primitive_gates/nand1.desc index 2b5bbef22..da1db3f8c 100644 --- a/regression/verilog/primitive_gates/nand1.desc +++ b/regression/verilog/primitive_gates/nand1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE nand1.sv --bound 0 ^EXIT=0$ diff --git a/regression/verilog/primitive_gates/xnor3.desc b/regression/verilog/primitive_gates/xnor3.desc index c0221a595..7f4836cde 100644 --- a/regression/verilog/primitive_gates/xnor3.desc +++ b/regression/verilog/primitive_gates/xnor3.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE xnor3.sv --bound 0 ^\[main\.xnor_ok\] always main\.xnor_in1 ~\^ main\.xnor_in2 == main\.xnor_out: PROVED up to bound 0$ diff --git a/regression/verilog/system-functions/low1.desc b/regression/verilog/system-functions/low1.desc index b345c1083..81145fc4a 100644 --- a/regression/verilog/system-functions/low1.desc +++ b/regression/verilog/system-functions/low1.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE low1.sv --module main --bound 0 ^EXIT=0$ diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 5f673cfe8..0997641e4 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -275,8 +275,7 @@ int ebmc_parse_optionst::doit() netlistt netlist; if(ebmc_base.make_netlist(netlist)) return 1; - auto filename = - cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-"; + auto filename = cmdline.value_opt("outfile").value_or("-"); output_filet outfile{filename}; outfile.stream() << "digraph netlist {\n"; netlist.output_dot(outfile.stream()); @@ -289,8 +288,7 @@ int ebmc_parse_optionst::doit() netlistt netlist; if(ebmc_base.make_netlist(netlist)) return 1; - auto filename = - cmdline.isset("outfile") ? cmdline.get_value("outfile") : "-"; + auto filename = cmdline.value_opt("outfile").value_or("-"); output_filet outfile{filename}; outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n'; outfile.stream() << "-- Generated from " diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 506c49351..939717f76 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -238,7 +238,6 @@ IREP_ID_ONE(verilog_time) IREP_ID_ONE(verilog_iff) IREP_ID_ONE(verilog_implies) IREP_ID_ONE(offset) -IREP_ID_ONE(xnor) IREP_ID_ONE(specify) IREP_ID_ONE(x) IREP_ID_ONE(verilog_empty_item) diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 94d1c6b94..646efcb4d 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -1572,11 +1572,9 @@ void verilog_synthesist::synth_module_instance_builtin( exprt op; if(instance.type().id() == ID_bool) - op = not_exprt{ - multi_ary_exprt{ID_xor, std::move(operands), instance.type()}}; + op = not_exprt{xor_exprt{std::move(operands)}}; else - op = bitnot_exprt{ - multi_ary_exprt{ID_bitxor, std::move(operands), instance.type()}}; + op = bitnot_exprt{bitxor_exprt{std::move(operands), instance.type()}}; equal_exprt constraint{output, std::move(op)}; trans.invar().add_to_operands(std::move(constraint)); From b20299af89854d3b409e90347b518fe395c1af1e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 1 Nov 2024 09:57:00 -0400 Subject: [PATCH 2/2] Verilog: use zero_extend_exprt This replaces two typecasts by zero_extend_exprt. --- src/verilog/aval_bval_encoding.cpp | 5 +++++ src/verilog/aval_bval_encoding.h | 3 +++ src/verilog/expr2verilog.cpp | 22 ++++++++++++++++++++++ src/verilog/expr2verilog_class.h | 2 ++ src/verilog/verilog_lowering.cpp | 14 ++++++++++++++ src/verilog/verilog_typecheck_expr.cpp | 23 +++++++---------------- 6 files changed, 53 insertions(+), 16 deletions(-) diff --git a/src/verilog/aval_bval_encoding.cpp b/src/verilog/aval_bval_encoding.cpp index 0636669aa..25f6e50bd 100644 --- a/src/verilog/aval_bval_encoding.cpp +++ b/src/verilog/aval_bval_encoding.cpp @@ -392,3 +392,8 @@ exprt aval_bval(const typecast_exprt &expr) auto op_aval_zero = to_bv_type(op_aval.type()).all_zeros_expr(); return and_exprt{not_exprt{op_has_xz}, notequal_exprt{op_aval, op_aval_zero}}; } + +exprt aval_bval(const zero_extend_exprt &expr) +{ + abort(); +} diff --git a/src/verilog/aval_bval_encoding.h b/src/verilog/aval_bval_encoding.h index 71fa49a3b..33078cea9 100644 --- a/src/verilog/aval_bval_encoding.h +++ b/src/verilog/aval_bval_encoding.h @@ -9,6 +9,7 @@ Author: Daniel Kroening, dkr@amazon.com #ifndef CPROVER_VERILOG_AVAL_BVAL_H #define CPROVER_VERILOG_AVAL_BVAL_H +#include #include #include @@ -58,5 +59,7 @@ exprt aval_bval(const verilog_iff_exprt &); exprt aval_bval(const verilog_implies_exprt &); /// lowering for typecasts exprt aval_bval(const typecast_exprt &); +/// lowering for zero extension +exprt aval_bval(const zero_extend_exprt &); #endif diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 1100f48bf..9c1d35983 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -773,6 +773,25 @@ expr2verilogt::resultt expr2verilogt::convert_explicit_size_cast( /*******************************************************************\ +Function: expr2verilogt::convert_zero_extend + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +expr2verilogt::resultt +expr2verilogt::convert_zero_extend(const zero_extend_exprt &src) +{ + // added by the type checker; igore + return convert_rec(src.op()); +} + +/*******************************************************************\ + Function: expr2verilogt::convert_index Inputs: @@ -1546,6 +1565,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) else if(src.id()==ID_typecast) return convert_typecast(to_typecast_expr(src)); + else if(src.id() == ID_zero_extend) + return convert_zero_extend(to_zero_extend_expr(src)); + else if(src.id()==ID_and) return convert_binary( to_multi_ary_expr(src), "&&", precedence = verilog_precedencet::AND); diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 15896451e..c7daa9df2 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -116,6 +116,8 @@ class expr2verilogt resultt convert_typecast(const typecast_exprt &); + resultt convert_zero_extend(const zero_extend_exprt &); + resultt convert_explicit_size_cast(const class verilog_explicit_size_cast_exprt &); diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp index 1631c94fc..d4ab33177 100644 --- a/src/verilog/verilog_lowering.cpp +++ b/src/verilog/verilog_lowering.cpp @@ -399,6 +399,20 @@ exprt verilog_lowering(exprt expr) else return expr; } + else if(expr.id() == ID_zero_extend) + { + auto &zero_extend = to_zero_extend_expr(expr); + + if( + is_four_valued(zero_extend.type()) || + is_four_valued(zero_extend.op().type())) + { + // encode into aval/bval + return aval_bval(zero_extend); + } + else + return expr; // leave as is + } else return expr; // leave as is diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 37fc4dcd4..dd98036b1 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2094,23 +2094,14 @@ Function: zero_extend 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); + exprt result = expr; + + if(expr.type().id() == ID_bool) + result = typecast_exprt{expr, unsignedbv_typet{1}}; + else if(expr.type().id() == ID_integer) + result = typecast_exprt{expr, unsignedbv_typet{32}}; - return typecast_exprt::conditional_cast( - typecast_exprt::conditional_cast(expr, tmp_type), type); + return zero_extend_exprt{std::move(result), type}; } /*******************************************************************\