From 783019ac742d0fed4fbcb4b7b9a66489e677d311 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 29 Dec 2018 12:46:51 +0000 Subject: [PATCH 1/3] smt2: fix for with on structs with one member --- src/solvers/smt2/smt2_conv.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 4f766d80e95..a3ece06d255 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3588,8 +3588,9 @@ void smt2_convt::convert_with(const with_exprt &expr) if(m.width==struct_width) { - // the struct is the same as the member, no concat needed - out << "?withop"; + // the struct is the same as the member, no concat needed, + // ?withop won't be used + convert_expr(value); } else if(m.offset==0) { From 1453075026e9a3c36c11e7ee4f45c7ff4d767c04 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 29 Dec 2018 12:47:04 +0000 Subject: [PATCH 2/3] smt2: fix typos in comments --- src/solvers/smt2/smt2_conv.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index a3ece06d255..c1c2a108fd2 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3476,7 +3476,7 @@ void smt2_convt::convert_with(const with_exprt &expr) { std::size_t s=expr.operands().size(); - // strip of the trailing two operands + // strip off the trailing two operands with_exprt tmp = expr; tmp.operands().resize(s-2); @@ -3515,7 +3515,7 @@ void smt2_convt::convert_with(const with_exprt &expr) std::size_t sub_width=boolbv_width(array_type.subtype()); std::size_t index_width=boolbv_width(expr.where().type()); - // We mask out the updated bit with AND, + // We mask out the updated bits with AND, // and then OR-in the shifted new value. out << "(let ((distance? "; From fbc74decc99fca2fa6de6dbebac9f71723212302 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 29 Dec 2018 13:04:55 +0000 Subject: [PATCH 3/3] smt2: fix with expressions for fixed-width arrays --- scripts/delete_failing_smt2_solver_tests | 3 --- src/solvers/smt2/smt2_conv.cpp | 11 ++++++----- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index 33f1b8a4417..4069e47cbb3 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -37,14 +37,12 @@ rm Float8/test.desc rm Linking4/test.desc rm Linking7/test.desc rm Linking7/member-name-mismatch.desc -rm Malloc19/test.desc rm Malloc23/test.desc rm Malloc24/test.desc rm Memory_leak2/test.desc rm Multi_Dimensional_Array2/test.desc rm Overflow_Leftshift1/test.desc rm Overflow_Subtraction1/test.desc -rm Pointer_Arithmetic10/test.desc rm Pointer_Arithmetic11/test.desc rm Pointer_byte_extract2/test.desc rm Pointer_byte_extract3/test.desc @@ -88,7 +86,6 @@ rm pointer-function-parameters-struct-simple-recursion-2/test.desc rm pointer-function-parameters-struct-simple-recursion-3/test.desc rm scanf1/test.desc rm stack-trace/test.desc -rm struct10/test.desc rm struct6/test.desc rm struct7/test.desc rm struct9/test.desc diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index c1c2a108fd2..19af8049cb9 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -3540,15 +3540,16 @@ void smt2_convt::convert_with(const with_exprt &expr) out << "(bvor "; out << "(bvand "; - out << "(bvlshr (_ bv" << power(2, array_width)-1 << " " - << array_width << ") "; - out << "distance?) "; + out << "(bvnot "; + out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width + << ") "; + out << "distance?)) "; // bvnot, bvlshl convert_expr(expr.old()); out << ") "; // bvand - out << "(bvlshr "; + out << "(bvshl "; out << "((_ zero_extend " << array_width-sub_width << ") "; convert_expr(expr.new_value()); - out << ") distance?)))"; // zero_extend, bvlshr, bvor, let + out << ") distance?)))"; // zero_extend, bvshl, bvor, let } } else if(expr_type.id()==ID_struct)