use optional for unknown pointer offset sizes #2137

kroening · 2018-04-28T17:37:35Z

This removes another case of using -1 as 'error value': pointer_offset_size and variants.

tautschnig

This looks good to me. I'd be curious to know whether there is any change in performance (positive or negative) for some of this code is called a lot.

tautschnig · 2018-04-29T18:22:19Z

src/analyses/goto_rw.cpp

+  if(offset_bits.has_value())
+    offset = to_range_spect(*offset_bits);
+  else
+    offset = -1;


Nit pick: use ? : as above instead of the if ... else

Merged with next branch

tautschnig · 2018-04-29T18:22:52Z

src/analyses/goto_rw.cpp

+    if(subtype_bits.has_value())
+      sub_size = to_range_spect(*subtype_bits);
+    else
+      sub_size = -1;


Use ? : as above.

tautschnig · 2018-04-29T18:23:03Z

src/analyses/goto_rw.cpp

+    if(subtype_bits.has_value())
+      sub_size = to_range_spect(*subtype_bits);
+    else
+      sub_size = -1;


Use ? : as above.

tautschnig · 2018-04-29T18:23:19Z

src/analyses/goto_rw.cpp

+  if(subtype_bits.has_value())
+    sub_size = to_range_spect(*subtype_bits);
+  else
+    sub_size = -1;


Use ? : as above.

Merged with next branch.

tautschnig · 2018-04-29T18:26:04Z

src/analyses/reaching_definitions.cpp

+      {
+        range_spect size = to_range_spect(*param_bits);
+        gen(from, identifier, 0, size);
+      }


No, this should invoke gen even when the size cannot be determined (using -1 as a value of size is well-defined).

tautschnig · 2018-04-29T18:29:48Z

src/goto-programs/vcd_goto_trace.cpp


-  if(width>=0)
-    return std::string(integer2size_t(width), 'x');
+  if(width.has_value() && *width >= 0)


The *width >= 0 is trivially true and should be removed.

kroening · 2018-04-30T09:15:15Z

Performance: I would expect a very minor positive effect (the comparison with of an mp_integer with -1 is mildly elaborate).

smowton

Mostly nitpicks but at least a couple of mistakes to fix

smowton · 2018-04-30T09:19:09Z

src/analyses/goto_rw.cpp

-      to_range_spect(pointer_offset_bits(vector_type.subtype(), ns));
+    auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
+
+    sub_size = subtype_bits.has_value()?to_range_spect(*subtype_bits):-1;


?: op spacing (also below)

smowton · 2018-04-30T11:10:09Z

src/pointer-analysis/value_set.cpp

-        if(comp_offset>op1_offset)
+        if(!comp_offset.has_value())
+          continue;
+        else if(comp_offset > op1_offset)


*comp_offset?

smowton · 2018-04-30T11:18:26Z

src/util/endianness_map.cpp

-  if(s<=0)
+  auto s = pointer_offset_bits(src, ns);
+
+  if(!s.has_value())


I had pondered this one as well, but it's actually ok as the loop simply turns into a no-op.

Ah true, though I suspect the original author intended to skip set-up for the loop in that case. That means the only proper error is the != vs. == problem below.

smowton · 2018-04-30T11:19:53Z

src/util/pointer_offset_size.cpp

-      return member_bits;
+    auto member_bits = pointer_offset_bits(comp.type(), ns);
+    if(!member_bits.has_value())
+      return optionalt<mp_integer>();


Can use {} as a shorthand if you prefer

smowton · 2018-04-30T11:26:57Z

src/util/simplify_expr.cpp

-      // no arrays of non-byte sized objects
-      assert(el_size%8==0);
-      mp_integer el_bytes=el_size/8;
+      DATA_INVARIANT(*el_size>0, "no arrays of zero-sized objects");


Rephrase as a "should" statement for clarity when printed as an error dump (as written it's not clear whether we're forbidding or complaining that no such array was found)

smowton · 2018-04-30T11:28:40Z

src/util/simplify_expr.cpp

@@ -2038,7 +2033,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
  const typet &op_type=ns.follow(root.type());

  // size must be known
-  if(val_size<=0)
+  if(!val_size.has_value() || *val_size != 0)


smowton · 2018-04-30T11:29:52Z

src/util/simplify_expr.cpp

+      {
+        result_expr.make_nil();
+        break;
+      }

      // can we determine the current offset, and is it a byte-sized


Comment belongs above, since the "can we determine" and the byte alignment question are now checked seperately

I think this is still wrong -- "Can we determine the current offset?" belongs above if(!m_offset.has_value() || ...), then "Is it a byte-sized member?" belongs here.

smowton · 2018-04-30T11:34:39Z

@kroening for the breakages that didn't cause a CI failure suggest adding a test case

peterschrammel · 2018-05-10T13:17:26Z

src/util/simplify_expr.cpp

-              m_offset>=offset_int+update_size)
+      else if(
+        update_size.has_value() && *update_size > 0 &&
+        *m_offset >= offset_int + *update_size)
        break;


consider putting braces around break (preceding multi-line conditional) to improve readability

peterschrammel · 2018-05-10T13:17:45Z

src/util/simplify_expr.cpp

+    auto el_size = pointer_offset_bits(op_type.subtype(), ns);
+    if(
+      !el_size.has_value() || *el_size == 0 || (*el_size) % 8 != 0 ||
+      (*val_size) % 8 != 0)
      return true;


consider putting braces around return (preceding multi-line conditional) to improve readability

peterschrammel · 2018-05-10T13:19:43Z

src/util/pointer_offset_size.cpp

+      if(
+        sub_size.has_value() && *sub_size > 0 &&
+        !to_integer(index_expr.index(), i))
+        return (*o) + i * (*sub_size);


consider putting braces around return (preceding multi-line conditional) to improve readability

peterschrammel · 2018-05-10T13:24:30Z

src/solvers/flattening/flatten_byte_operators.cpp

        throw "can't flatten byte_update for sub-type without size";

+      mp_integer sub_size = *sub_size_opt;


peterschrammel · 2018-05-10T13:26:03Z

src/solvers/flattening/flatten_byte_operators.cpp

    throw "byte_update of unknown width:\n"+src.pretty();

+  mp_integer element_size = *element_size_opt;


peterschrammel · 2018-05-10T13:32:24Z

src/goto-symex/symex_builtin_functions.cpp

        mp_integer alloc_size;

-        if(elem_size<0)


I think there was some value in the != 0 check here as we are going to divide by elem_size later on, but that might already be implied by an invariant of pointer_offset_size().

smowton

One nitpick, otherwise lgtm.

smowton · 2018-05-14T07:50:37Z

src/util/simplify_expr.cpp

+      {
+        result_expr.make_nil();
+        break;
+      }

      // can we determine the current offset, and is it a byte-sized


I think this is still wrong -- "Can we determine the current offset?" belongs above if(!m_offset.has_value() || ...), then "Is it a byte-sized member?" belongs here.

kroening · 2018-05-14T17:50:19Z

Fixed the comment

kroening · 2018-05-22T15:05:46Z

There is performance cost:

#include "optional.h"
#include "mp_arith.h"

optionalt<mp_integer> some_a(long long i)
{
  if(i%2)
    return {};
  else
    return mp_integer(i);
}

mp_integer some_b(long long i)
{
  if(i%2)
    return -1;
  else
    return i;
}

int main()
{
  long long j=0;
  for(long long i=0; i<20000000; i++)
  {
    //if(some_a(i).has_value()) j++;
    if(some_b(i)!=-1) j++;
  }
}

With -O2 or -O3 the difference is 1.50s vs. 1.24s

kroening · 2018-06-14T10:35:20Z

Rebased.

tautschnig · 2018-08-12T19:00:11Z

@kroening Could you please rebase again? With the continuous evaluation set-up prepared by @peterschrammel we should surely notice if this change truly results in a performance impact.

kroening · 2018-08-24T09:43:39Z

Rebase done.

allredj

Passed Diffblue compatibility checks (cbmc commit: 4568839).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85642915

kroening · 2018-09-30T11:43:00Z

New data, on Linux:

clang++ 3.5.0 -O2:
with optionalt: 0.58s
with -1: 0.65s

clang++ 6.0.1 -O2:
with std::optional: 0.54s
with optionalt: 0.54s
with -1: 0.61s

g++ 8.2.0 -O2:
with std::optional: 0.61s
with optionalt: 0.59s
with -1: 0.66s

I.e., this delivers a performance improvement on Linux. Will merge once CIed.

allredj

Passed Diffblue compatibility checks (cbmc commit: 3f59028).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86391538

kroening requested a review from tautschnig April 28, 2018 17:37

kroening requested review from chrisr-diffblue, martin-cs, peterschrammel, smowton and thk123 as code owners April 28, 2018 17:37

kroening added the cleanup label Apr 28, 2018

kroening force-pushed the optional_pointer_offset branch 4 times, most recently from 2a7f009 to aac7dd7 Compare April 29, 2018 14:36

tautschnig reviewed Apr 29, 2018

View reviewed changes

kroening force-pushed the optional_pointer_offset branch from aac7dd7 to 4964eb2 Compare April 30, 2018 09:11

kroening force-pushed the optional_pointer_offset branch from 4964eb2 to 2621da2 Compare April 30, 2018 09:46

kroening assigned tautschnig Apr 30, 2018

smowton suggested changes Apr 30, 2018

View reviewed changes

kroening force-pushed the optional_pointer_offset branch from 2621da2 to fe9223e Compare April 30, 2018 14:47

peterschrammel reviewed May 10, 2018

View reviewed changes

kroening force-pushed the optional_pointer_offset branch from fe9223e to 3b89aa5 Compare May 12, 2018 13:19

kroening assigned peterschrammel, smowton and tautschnig and unassigned tautschnig and peterschrammel May 12, 2018

smowton approved these changes May 14, 2018

View reviewed changes

kroening force-pushed the optional_pointer_offset branch from 3b89aa5 to 03aceea Compare May 14, 2018 17:49

kroening force-pushed the optional_pointer_offset branch 3 times, most recently from 53e10d9 to f06e62e Compare June 7, 2018 14:04

kroening force-pushed the optional_pointer_offset branch from f06e62e to 5ff66cb Compare June 14, 2018 10:34

kroening force-pushed the optional_pointer_offset branch from 5ff66cb to bd5e6d8 Compare July 6, 2018 09:04

kroening requested a review from pkesseli as a code owner July 6, 2018 09:04

tautschnig approved these changes Aug 12, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Aug 12, 2018

tautschnig added the Needs rebase label Aug 12, 2018

kroening force-pushed the optional_pointer_offset branch from bd5e6d8 to 3d811f0 Compare August 24, 2018 09:43

kroening removed the Needs rebase label Aug 24, 2018

kroening force-pushed the optional_pointer_offset branch 2 times, most recently from 28f0abe to efdc901 Compare August 24, 2018 17:09

kroening force-pushed the optional_pointer_offset branch from efdc901 to 4568839 Compare September 22, 2018 17:13

kroening assigned peterschrammel and unassigned kroening Sep 22, 2018

allredj reviewed Sep 22, 2018

View reviewed changes

peterschrammel assigned kroening and unassigned peterschrammel Sep 24, 2018

use optional for unknown pointer offset sizes

3f59028

kroening force-pushed the optional_pointer_offset branch from 4568839 to 3f59028 Compare September 30, 2018 11:05

allredj reviewed Sep 30, 2018

View reviewed changes

tautschnig merged commit 8401f49 into develop Sep 30, 2018

tautschnig deleted the optional_pointer_offset branch September 30, 2018 13:59

		throw "can't flatten byte_update for sub-type without size";

		mp_integer sub_size = *sub_size_opt;

		throw "byte_update of unknown width:\n"+src.pretty();

		mp_integer element_size = *element_size_opt;

use optional for unknown pointer offset sizes #2137

use optional for unknown pointer offset sizes #2137

Uh oh!

Conversation

kroening commented Apr 28, 2018

Uh oh!

tautschnig left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Apr 30, 2018

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Apr 30, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented May 14, 2018

Uh oh!

kroening commented May 22, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kroening commented Jun 14, 2018

tautschnig left a comment •

edited

Loading

kroening commented May 22, 2018 •

edited

Loading