From 2d72002088c002bd35dac6111b3e37111dd90474 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 13 Feb 2019 12:31:49 +0000 Subject: [PATCH 1/4] build_object_descriptor: avoid redundant typecasts These can fool later simplifications by appearing to be non-constant. --- src/util/std_expr.cpp | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index c549178259f..e9f32cc0f2c 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -72,10 +72,11 @@ static void build_object_descriptor_rec( exprt sub_size=size_of_expr(expr.type(), ns); CHECK_RETURN(sub_size.is_not_nil()); - dest.offset()= - plus_exprt(dest.offset(), - mult_exprt(typecast_exprt(index.index(), index_type()), - typecast_exprt(sub_size, index_type()))); + dest.offset() = plus_exprt( + dest.offset(), + mult_exprt( + typecast_exprt::conditional_cast(index.index(), index_type()), + typecast_exprt::conditional_cast(sub_size, index_type()))); } else if(expr.id()==ID_member) { @@ -87,9 +88,8 @@ static void build_object_descriptor_rec( exprt offset=member_offset_expr(member, ns); CHECK_RETURN(offset.is_not_nil()); - dest.offset()= - plus_exprt(dest.offset(), - typecast_exprt(offset, index_type())); + dest.offset() = plus_exprt( + dest.offset(), typecast_exprt::conditional_cast(offset, index_type())); } else if(expr.id()==ID_byte_extract_little_endian || expr.id()==ID_byte_extract_big_endian) @@ -100,10 +100,10 @@ static void build_object_descriptor_rec( build_object_descriptor_rec(ns, be.op(), dest); - dest.offset()= - plus_exprt(dest.offset(), - typecast_exprt(to_byte_extract_expr(expr).offset(), - index_type())); + dest.offset() = plus_exprt( + dest.offset(), + typecast_exprt::conditional_cast( + to_byte_extract_expr(expr).offset(), index_type())); } else if(expr.id()==ID_typecast) { From 992a3c39fe4f84cd0e07ec279f051f735b440f52 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 13 Feb 2019 13:22:25 +0000 Subject: [PATCH 2/4] Simplify object descriptor offset after construction Leaving this with trivially simplifiable expressions such as (0 + 0) means subsequent simplifications that check for offset.is_constant() may be wrongly skipped. --- src/util/std_expr.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index e9f32cc0f2c..a6a30ba4ea0 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_util.h" #include "mathematical_types.h" #include "pointer_offset_size.h" +#include "simplify_expr.h" bool constant_exprt::value_is_zero_string() const { @@ -145,6 +146,7 @@ void object_descriptor_exprt::build( offset()=from_integer(0, index_type()); build_object_descriptor_rec(ns, expr, *this); + simplify(offset(), ns); } shift_exprt::shift_exprt( From 8c231e96deda90fff2b35db505f626bb4042a2fa Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 14 Feb 2019 08:45:54 +0000 Subject: [PATCH 3/4] Generics unit test: set integer widths This test indirectly uses object_descriptor_exprt, which uses simplify_sum, which in turn requires integer constants to have defined widths. --- .../java_bytecode/goto_program_generics/generic_bases_test.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp index 769edb50a13..2f007b2fa25 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp @@ -21,6 +21,8 @@ SCENARIO( "Instantiate generic parameters of superclasses", "[core][goto_program_generics][generic_bases_test]") { + config.ansi_c.set_LP64(); + GIVEN( "A class extending a generic class instantiated with a standard library " "class") From 7d0ce455edb18026439f509a70f4fdf8673f4ecd Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 14 Feb 2019 08:54:58 +0000 Subject: [PATCH 4/4] Remove now-unnecessary simplify after object_descriptor_exprt::build --- src/goto-symex/symex_clean_expr.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 6b787375818..6584b7dd3cc 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -72,8 +72,6 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns) { object_descriptor_exprt ode; ode.build(expr, ns); - if(do_simplify) - simplify(ode.offset(), ns); expr = ode.root_object();