From 7857669435b18d97c98ececf1bfdeb0e77358a3d Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 12 Sep 2018 09:01:46 +0100 Subject: [PATCH 1/4] Correct input initialization in builtin function Result was moved twice instead of initializing `input` field with the given `input`. --- src/solvers/refinement/string_builtin_function.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h index c53137a243f..7338d38363d 100644 --- a/src/solvers/refinement/string_builtin_function.h +++ b/src/solvers/refinement/string_builtin_function.h @@ -83,7 +83,7 @@ class string_transformation_builtin_functiont : public string_builtin_functiont array_string_exprt input) : string_builtin_functiont(std::move(return_code)), result(std::move(result)), - input(std::move(result)) + input(std::move(input)) { } From 207ca8ce934b8b3f3173e4a22f133b59a7db717c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 7 Sep 2018 15:25:50 +0200 Subject: [PATCH 2/4] Support null-pointer without operand in interpreter --- src/goto-programs/interpreter_evaluate.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index b53af16a95f..c144a4f4309 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -339,7 +339,15 @@ void interpretert::evaluate( evaluate(expr.op0(), dest); return; } - if(expr.has_operands() && !to_integer(expr.op0(), i)) + else if(expr.has_operands() && !to_integer(expr.op0(), i)) + { + dest.push_back(i); + return; + } + // check if expression is constant null pointer without operands + else if( + !expr.has_operands() && !to_integer(to_constant_expr(expr), i) && + i.is_zero()) { dest.push_back(i); return; From df6c64f8b1e493819715075cbe028ed66535f2f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Mon, 10 Sep 2018 15:35:36 +0200 Subject: [PATCH 3/4] Remove ID_address_of check for types as it can only be exprt --- src/goto-programs/interpreter.cpp | 3 +-- src/goto-programs/interpreter_evaluate.cpp | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index fa9617dfb0b..ccfe7e0070b 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -600,7 +600,7 @@ exprt interpretert::get_value( { return from_integer(rhs[integer2size_t(offset)]!=0?1:0, type); } - else if((real_type.id()==ID_pointer) || (real_type.id()==ID_address_of)) + else if(real_type.id() == ID_pointer) { if(rhs[integer2size_t(offset)]==0) { @@ -1090,4 +1090,3 @@ void interpreter( message_handler); interpreter(); } - diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index c144a4f4309..71349a5734b 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -330,8 +330,7 @@ void interpretert::evaluate( dest.clear(); } - else if((expr.type().id()==ID_pointer) - || (expr.type().id()==ID_address_of)) + else if(expr.type().id() == ID_pointer) { mp_integer i=0; if(expr.has_operands() && expr.op0().id()==ID_address_of) From f7e9715588aba6be08a5b32733a42efc2123054a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 11 Sep 2018 10:03:02 +0200 Subject: [PATCH 4/4] Add unit test for interpreter evaluation --- src/goto-programs/interpreter_class.h | 2 + unit/Makefile | 1 + unit/interpreter/interpreter.cpp | 72 ++++++++++++++++++++++++ unit/interpreter/module_dependencies.txt | 3 + 4 files changed, 78 insertions(+) create mode 100644 unit/interpreter/interpreter.cpp create mode 100644 unit/interpreter/module_dependencies.txt diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 04b3d32446d..e0fefe283f9 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -306,6 +306,8 @@ class interpretert:public messaget void initialize(bool init); void show_state(); + + friend class interpreter_testt; }; #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H diff --git a/unit/Makefile b/unit/Makefile index a8c8d3dc60d..fa9c96aac4b 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -45,6 +45,7 @@ SRC += unit_tests.cpp \ util/symbol_table.cpp \ util/unicode.cpp \ catch_example.cpp \ + interpreter/interpreter.cpp \ # Empty last line INCLUDES= -I ../src/ -I. diff --git a/unit/interpreter/interpreter.cpp b/unit/interpreter/interpreter.cpp new file mode 100644 index 00000000000..4278d80a4d5 --- /dev/null +++ b/unit/interpreter/interpreter.cpp @@ -0,0 +1,72 @@ +/*******************************************************************\ + + Module: Interpreter unit tests. + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +typedef interpretert::mp_vectort mp_vectort; + +class interpreter_testt +{ + symbol_tablet symbol_table; + goto_functionst goto_functions; + null_message_handlert null_message_handler; + interpretert interpreter; + +public: + explicit interpreter_testt() + : interpreter(symbol_table, goto_functions, null_message_handler) + { + } + + mp_vectort evaluate(const exprt &expression) + { + mp_vectort result; + interpreter.evaluate(expression, result); + return result; + } +}; + +SCENARIO("interpreter evaluation null pointer expressions") +{ + interpreter_testt interpreter_test; + mp_vectort null_vector = {0}; + + THEN("null pointer without operands") + { + unsignedbv_typet java_char(16); + pointer_typet pointer_type(java_char, 64); + + constant_exprt constant_expr(ID_NULL, pointer_type); + + mp_vectort mp_vector = interpreter_test.evaluate(constant_expr); + + REQUIRE_THAT(mp_vector, Catch::Equals(null_vector)); + } + THEN("null pointer with operands") + { + pointer_typet outer_pointer_type(empty_typet(), 64); + constant_exprt outer_expression( + "0000000000000000000000000000000000000000000000000000000000000000", + outer_pointer_type); + + pointer_typet inner_pointer_type(empty_typet(), 64); + constant_exprt inner_expression(ID_NULL, inner_pointer_type); + + outer_expression.move_to_operands(inner_expression); + + mp_vectort mp_vector = interpreter_test.evaluate(outer_expression); + + REQUIRE_THAT(mp_vector, Catch::Equals(null_vector)); + } +} diff --git a/unit/interpreter/module_dependencies.txt b/unit/interpreter/module_dependencies.txt new file mode 100644 index 00000000000..070c3bcc8bb --- /dev/null +++ b/unit/interpreter/module_dependencies.txt @@ -0,0 +1,3 @@ +goto-programs +testing-utils +util