Floating point simplification for goto-analyzer constants domain #2081

hannes-steffenhagen-diffblue · 2018-04-17T16:13:21Z

This

moves adjust_float_expression from symex to goto-programs - it only depends on stuff from util and goto-programs, so this should be fine
uses adjust_float_expression in the constant propagator domain
The functions from fenv.h (fesetround etc) are not used in the regression tests because apparently they don't quite work in goto-analyzer at the moment (implementation doesn't seem to be visible?)

tautschnig

I don't quite understand "The functions from fenv.h (fesetround etc) are not used in the regression tests because apparently they don't quite work in goto-analyzer at the moment (implementation doesn't seem to be visible?)" -- is it the implementation from the built-in C library that you are hoping for? That code is currently #if 0 in goto_analyzer_parse_options.cpp.

tautschnig · 2018-04-17T23:57:47Z

src/goto-programs/Makefile

@@ -69,6 +69,7 @@ SRC = basic_blocks.cpp \
      wp.cpp \
      write_goto_binary.cpp \
      xml_goto_trace.cpp \
+      adjust_float_expressions.cpp \


Please retain lexicographic ordering.

tautschnig · 2018-04-18T00:01:18Z

src/goto-programs/adjust_float_expressions.cpp

+    expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
+    expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div ||
+    expr.id() == ID_floatbv_div || expr.id() == ID_floatbv_rem ||
+    expr.id() == ID_floatbv_typecast)


I would strongly encourage a plain move without reformatting.

Without reformatting this won't pass CI as it's picked up by git-clang-format - or do you mean doing the move and the reformatting in separate commits?

The clang-format stage is marked as allow_failures, so you don't actually have to make it succeed.

tautschnig · 2018-04-18T00:01:47Z

src/goto-programs/adjust_float_expressions.h

-void adjust_float_expressions(
-  exprt &expr,
-  const namespacet &ns);
+void adjust_float_expressions(exprt &expr, const namespacet &ns);


As above, I'd advise against reformatting.

Hi @tautschnig. How strongly do you object to the reformatting of these files? The rationale for the changes is that since they are getting moved anyway, we might as well just reformat them to the new automatically enforced style. This is a notion I find myself agreeing with.

Why is it a problem if we do it? If it's truly a problem, how do you suggest we rectify the situation?

There are three contexts of why this is a problem:

Reviewing is somewhere between impossible and impractical.

If anyone else has patches against those files, whether currently under review in some PR or completely out-of-tree, then any attempt to rebase or merge will require a rewrite of the patches. At bare minimum it is necessary to split the move of the file and adjustments to formatting into separate commits.

Trying to track down the rationale of some lines of code via git blame becomes a lot harder.

And all that with no known benefit on the plus side.

I'd agree with @tautschnig - keep a move as a pure move as much as possible.

That's fair, I'll undo the formatting

tautschnig · 2018-04-18T00:02:39Z

src/jbmc/jbmc_parse_options.cpp

@@ -44,7 +44,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_symbol_table.h>
 #include <goto-programs/show_properties.h>

-#include <goto-symex/adjust_float_expressions.h>
+#include <goto-programs/adjust_float_expressions.h>


The blank line above that can now go away for it's no longer a separate group/directory.

tautschnig · 2018-04-18T00:04:11Z

src/cbmc/cbmc_parse_options.cpp

@@ -52,7 +52,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/string_instrumentation.h>

 #include <goto-symex/rewrite_union.h>
-#include <goto-symex/adjust_float_expressions.h>
+#include <goto-programs/adjust_float_expressions.h>


This belongs in the group one above now. (Well, rewrite_union should likely be moved to goto-programs as well.)

tautschnig · 2018-04-18T00:04:46Z

src/goto-diff/goto_diff_parse_options.cpp

@@ -47,7 +47,7 @@ Author: Peter Schrammel
 #include <goto-programs/link_to_library.h>

 #include <goto-symex/rewrite_union.h>
-#include <goto-symex/adjust_float_expressions.h>
+#include <goto-programs/adjust_float_expressions.h>


As above: move one group up.

tautschnig · 2018-04-18T00:05:33Z

regression/goto-analyzer/constant_propagation_floating_point_div/test.desc

+^SIGNAL=0$
+^\[main.assertion.1\] file main.c line 8 function main, assertion eight == 8: Success$
+--
+^warning: ignoring


GitHub says there is no newline.

tautschnig · 2018-04-18T00:06:07Z

regression/goto-analyzer/constant_propagation_rounding_mode/test.desc

@@ -0,0 +1,10 @@
+


Spurious blank line?

tautschnig · 2018-04-18T00:06:20Z

regression/goto-analyzer/constant_propagation_rounding_mode/test.desc

+^\[main.assertion.1\] file main.c line 9 function main, assertion rounded_up - 0.1f >= 0: Success
+^\[main.assertion.2\] file main.c line 10 function main, assertion rounded_down - 0.1f < 0: Success
+--
+^warning: ignoring


Missing newline.

hannes-steffenhagen-diffblue · 2018-04-18T10:03:08Z

@tautschnig Yes, I meant I'm not using them because goto-analyzer currently doesn't handle them. I've addressed the formatting and the broken regression test, except for avoiding move+format.

hannes-steffenhagen-diffblue · 2018-04-18T16:54:04Z

I've added some more code that tries to go through all rounding modes to see if the result is exact in case the rounding mode is unknown

hannes-steffenhagen-diffblue · 2018-04-18T18:28:12Z

Travis build fails because of some minor issue with braces (std::array, a bit confusingly, requires two pairs of braces because its a struct with an array inside).

I will not have the time to work on this in the next couple of days.

NlightNFotis

LGTM

hannes-steffenhagen-diffblue · 2018-05-03T12:10:25Z

@tautschnig I've renamed the try_evaluate procedure to partial_evaluate.

tautschnig · 2018-05-03T12:34:52Z

I've renamed the try_evaluate procedure to partial_evaluate.

Has this ended up in the wrong commit? Looking at the first commit, it still introduces try_evaluate, while at the end it looks fine. Could you please check?

tautschnig · 2018-05-03T12:43:06Z

src/util/irep_ids.def

@@ -665,6 +665,7 @@ IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
 IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation)
 IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation)
 IREP_ID_ONE(annotations)
+IREP_ID_TWO(cprover_rounding_mode, __CPROVER_rounding_mode)


Please don't put any hardcoded __CPROVER in here. See above for how to do it instead.

'll do this, but can you please explain why? Is it just to make the CPROVER_PREFIX configurable?

Yes. You might argue that there is a lot more that needs cleanup in this regard, but let's at least not introduce it in even more places. (I think we've got an issue open to do this cleanup.)

tautschnig · 2018-05-03T12:46:26Z

src/analyses/constant_propagator.cpp

+  // if the current rounding mode is top we can
+  // still get a non-top result by trying all rounding
+  // modes and checking if the results are all the same
+  if(!values.is_constant(symbol_exprt(ID_cprover_rounding_mode)))


Please use CPROVER_PREFIX "rounding_mode", although it might be good to create a central #define for this purpose, probably in ieee_float.h.

tautschnig · 2018-05-03T12:46:48Z

src/analyses/constant_propagator.cpp

+  {
+    constant_propagator_domaint child(*this);
+    child.values.set_to(
+      ID_cprover_rounding_mode,


See comment above.

hannes-steffenhagen-diffblue · 2018-05-04T09:21:27Z

@tautschnig I was planning on squashing the "domain" commits when this goes through review, so I'd only have a "move adjust_float_expressions" and a "add floating point support in constants domain" commit.

tautschnig · 2018-05-04T09:49:59Z

Thanks a lot for the clarifications regarding commit history! I'm happy to approve once the ID_cprover_rounding_mode is gone as indicated.

hannes-steffenhagen-diffblue · 2018-05-04T10:44:05Z

@tautschnig I moved ID_cprover_rounding_mode to ieee_float.h and defined it in terms of CPROVER_PREFIX, is that ok with you?

tautschnig · 2018-05-04T11:07:48Z

src/util/ieee_float.h


 class constant_exprt;
 class floatbv_typet;

+const irep_idt ID_cprover_rounding_mode = CPROVER_PREFIX "rounding_mode";


I think this should be ok, but it does come with the caveat that the order of static initialisation is not defined and therefore the number of the entry that it receives in the string table may vary.

Not only that, but statements like these often end up being initialised before the string table is created at all, leading to a segfault during static init. Suggest instead either a static function local (executed the first time the function runs) or directly defining this in irep_ids.def.

Ah, good point on the table initialisation, hadn't thought about that. I'd originally wanted to put it into irep_ids.def, but there's currently no way to make this work with the CPROVER prefix. I think it could be added, but I'll probably just have this a local for now.

tautschnig

I'd be happier with a #define some_name CPROVER_PREFIX "rounding_mode", but it's not a blocker.

chrisr-diffblue

I'm happy with this set of commits - thanks for taking the time to address all the review comments.

smowton

The static init is dangerous; otherwise lgtm.

smowton · 2018-05-14T15:09:39Z

src/analyses/constant_propagator.cpp

+     // NOLINTNEXTLINE (whitespace/braces)
+     ieee_floatt::ROUND_TO_PLUS_INF}};
+  exprt first_result;
+  for(std::size_t i = 0; i < rounding_modes.size(); ++i)


Worth commenting that this boils down to "if the result is the same in all rounding modes, return that; otherwise, report failure".

smowton · 2018-05-14T15:12:38Z

src/util/ieee_float.h


 class constant_exprt;
 class floatbv_typet;

+const irep_idt ID_cprover_rounding_mode = CPROVER_PREFIX "rounding_mode";


Not only that, but statements like these often end up being initialised before the string table is created at all, leading to a segfault during static init. Suggest instead either a static function local (executed the first time the function runs) or directly defining this in irep_ids.def.

hannes-steffenhagen-diffblue · 2018-05-15T12:54:52Z

@smowton Using a string constant instead of a irep_idt constant now, which shouldn't have the static initialisation problem. Also added some documentation to partial_evaluate_with_all_rounding_modes.

smowton

You can actually do one better with something like

irep_idt get_rounding_mode_id()
{
  static irep_idt rounding_mode_id = CPROVER_PREFIX "rounding_mode";
  return rounding_mode_id;
}

However the version proposed now is at least safe, so I'll lift my blocking review.

For rounding modes in constant propagator domain

martin-cs · 2018-05-17T14:50:32Z

regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c

+  __CPROVER_rounding_mode = nondet_rounding_mode();
+  // depending on rounding mode 1.0f/10.0f could
+  // be greater or smaller than 0.1
+


I disagree with the comment. 1.0f/10.0f will either be equal or less than f;

The division produces a repeating bit-string. h denotes the hidden bit, m are the 23 bits of significand that single precision float stores, g is the guard bit, s is the stick bits. As g = 1, s = 1, it rounds up giving

1.10011001100110011001100110011... h.mmmmmmmmmmmmmmmmmmmmmmmgsssss 10011001100110011001101

Round towards zero or round towards zero will round down giving the result 1 ulp less.

I disagree with the comment. 1.0f/10.0f will either be equal or less than f;

That's what I meant to say. FE_TONEAREST (default) and FE_UPWARD will yield the same result (slightly bigger than 0.1) and FE_DOWNWARD and FE_TOWARDZERO will also yield the same result (slightly less than 0.1). So overall, the result could either be slightly less than 0.1 or slightly more than 0.1 (but not more than f).

I see what you are getting at but in this case 0.1 is quite ambiguous. You might say "the real value of 0.1" or something similar.

Ah yes, 0.1 is meant to be 0.1 as in the real number, not any floating point approximation of it.

I would be grateful if you can add a comment to clarify that. Also, see the general point that if you want specific floating-point numbers, hex format is the most reliable way to specify them.

martin-cs · 2018-05-17T15:58:27Z

regression/goto-analyzer/constant_propagation_rounding_mode/main.c

+
+int main(void)
+{
+  __CPROVER_rounding_mode = 0;


Please don't use the numbers, use the C standard names for them FE_UPWARD and FE_DOWNWARD.

Yes, but the values for them are implementation defined and I can't use fesetround because it doesn't have a visible implementation in goto-analyzer. I could add a couple of defines like #define FE_TONEAREST 0 though if you think that'd improve readability.

fesetround should work so you can use the macros. Redefining them will likely cause problems.

fesetround doesn't work for me; If I call it with anything all the __CPROVER variables just become top immediately. I believe @tautschnig mentioned the math library is disabled in goto-analyzer or something along those lines?

This sounds like a bug that should be fixed rather than working around. There are a couple of possible causes:

the libraries are not loaded in goto-analyze.

they are but the domain is not handling them correctly.

IIRC --show-goto-program should be after program loading and thus make 1 obvious. --show should show the effect of analysis and so should identify 2.

@martin-cs So I've checked. If I add src/ansi-c/library/fenv.c to the mix I can indeed use fesetround, so the problem is that goto-analyzer isn't loading the libraries for some reason.

Do you get the same issue with both Makefile and CMake based builds? Probably goto-analyzer needs to link against the ansi-c library/dependency if it's not already doing so?

It's pretty basic, I think: link_to_library(goto_model, ui_message_handler); is #if 0'ed.

martin-cs · 2018-05-17T16:00:22Z

regression/goto-analyzer/constant_propagation_rounding_mode/main.c

+{
+  __CPROVER_rounding_mode = 0;
+  float rounded_up = 1.0f / 10.0f;
+  __CPROVER_rounding_mode = 1;


Names not numbers here!

martin-cs · 2018-05-17T16:01:38Z

regression/goto-analyzer/constant_propagation_rounding_mode/main.c

+  float rounded_up = 1.0f / 10.0f;
+  __CPROVER_rounding_mode = 1;
+  float rounded_down = 1.0f / 10.0f;
+  assert(rounded_up - 0.1f >= 0);


I don't know if this is intentional but this covers an awful lot of the C standard as it raises the question of what rounding mode is used for (compile time) constants!

Ah yes. I don't believe the C standard requires a particular rounding mode to be used for constants folding (only reference I found to that was this in section 6.6 of the C99 draft standard:

If a floating
expression is evaluated in the translation environment, the arithmetic precision and range
shall be at least as great as if the expression were being evaluated in the execution
environment.

In gcc these exact examples won't work for this reason, because it folds the constants at compile time; Which can be worked around with -O0 by putting the division by ten in a function. In goto-analyzer we don't fold the constants before analysis, of course if we ever do these tests might break.

OK. Can I suggest that you use the hex format if you mean a particular float.

0x1.99999ap-4f is the single precision float above / rounded up from the real value of 1 / 10.
0x1.999998p-4f is the one below.

martin-cs · 2018-05-17T16:02:50Z

regression/goto-analyzer/constant_propagation_rounding_mode/main.c

+  float rounded_down = 1.0f / 10.0f;
+  assert(rounded_up - 0.1f >= 0);
+  assert(rounded_down - 0.1f < 0);
+  return 0;


assert(rounded_down == 0.1f || rounded_up == 0.1f)

Should be true!

The literal 0.1f is in this case going to be the same as 1/10.0f rounded up because of how we treat literals, so 1/10.0f != 0.1f in this case.

Yes; my point is to document that one or the other is true.

martin-cs · 2018-05-17T16:08:49Z

src/analyses/constant_propagator.cpp

+     ieee_floatt::ROUND_TO_ZERO,
+     ieee_floatt::ROUND_TO_MINUS_INF,
+     // NOLINTNEXTLINE (whitespace/braces)
+     ieee_floatt::ROUND_TO_PLUS_INF}};


I believe this to be correct... but is it optimal? I think that ROUND_TO_*_INF should be sufficient.

Not necessarily, an expression may involve various floating point subexpressions that react differently to different rounding modes - for example, you might have two subexpressions where ROUND_TO_ZERO might lead to one of them being rounded up because its negative and the other being rounded down because its positive.

Yes; fair point. Each individual operation is equal to either round up or down, but the whole operation may not be.

martin-cs · 2018-05-17T16:10:24Z

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -477,6 +478,7 @@ int goto_analyzer_parse_optionst::doit()
 /// Depending on the command line mode, run one of the analysis tasks
 int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 {
+  adjust_float_expressions(goto_model);


I'm not sure if it is best to do this here or in the evaluation. How does this work with simplify and dump-c?

I'm honestly not 100% sure how goto-analyzer works, but

#include <assert.h> #include <fenv.h> float div_by_ten(float x) { return x/10.0f; } int main(void) { float f = 1.0f/10.0f; __CPROVER_rounding_mode = 1; float g = 1.0f/10.0f; assert(g < f); __CPROVER_rounding_mode = 3; float h = 1.0f/10.0f; assert(g == h); assert(h < f); __CPROVER_rounding_mode = 2; float i = 1.0f/10.0f; assert(f == i); }

putting this into goto-analyzer --simplify followed by --dump-c gives me

Reading GOTO program from `test.out' #include <assert.h> // div_by_ten // file test.c line 4 float div_by_ten(float x); // div_by_ten // file test.c line 4 float div_by_ten(float x) { return FLOAT/(x, 10.0f, __CPROVER_rounding_mode); } // main // file test.c line 8 signed int main(void) { float f=0.1f; __CPROVER_rounding_mode = 1; float g=0.1f; /* assertion g < f */ assert((_Bool)1); __CPROVER_rounding_mode = 3; float h=0.1f; /* assertion g == h */ assert((_Bool)1); /* assertion h < f */ assert((_Bool)1); __CPROVER_rounding_mode = 2; float i=0.1f; /* assertion f == i */ assert((_Bool)1); }

which should be correct.

The problem is that it has the (internal) rounded float exprs rather than the correct ones. Please adjust the float expressions during evaluation, not in the program.

Maybe @martin-cs will hate me for that, but ... how about a final cleanup step that removes all the internal ones? Much like is now done for remove_returns -> restore_returns.

The expression is already being modified during evaluation (substituting constants, calling simplify, etc.), so one more modification there won't hurt. Doing it up front requires changing it one way and then changing it back at the end.

Ok, but I have to clearly admit that it was me pushing @hannes-steffenhagen-diffblue in this direction with the rationale that repeated modifications would seem costly. With the added learnings ever since I am happy to backtrack on this. My bad.

Also my apologies to @hannes-steffenhagen-diffblue for not being more present in this one.

31ef182 Merge pull request diffblue#2208 from diffblue/cleanout-goto-programs 0e84d3e Merge pull request diffblue#2195 from smowton/smowton/feature/smarter-reachability-slicer c801126 Merge pull request diffblue#2209 from diffblue/travis-no-osx-g++ 3487bf7 Reachability slicer: mark reachable code more precisely 85e8451 Merge pull request diffblue#2066 from tautschnig/bv-endianness 5e5eafb Merge pull request diffblue#2191 from smowton/smowton/feature/java-fatal-assertions 8a68ab8 remove g++ build on OS X; this is identical to the clang++ build 48e5b25 Amend faulty long-string test 3f718ba Java: make null-pointer and similar checks fatal 821eb1d remove basic_blocks and goto_program_irep d87c2db Merge pull request diffblue#2203 from diffblue/typed-lookup d77dea3 strongly type the lookup() methods in namespacet 2382f27 Merge pull request diffblue#2193 from martin-cs/feature/correct-instruction-documentation c314272 Merge pull request diffblue#2181 from diffblue/format-expr-constants 514a0a5 Merge pull request diffblue#2167 from diffblue/parse_unwindset_options 0102452 move escape(s) to string_utils f1b6174 use unwindsett in goto-instrument dcc907a introduce unwindsett for unwinding limits 10aeae8 format_expr now does index, c_bool constants, string constants 92b92d6 Correct the documentation of ASSERT : it does not alter control flow. a11add8 Expand the documentation of the goto-program instructions. a06503b Merge pull request diffblue#2197 from tautschnig/fix-help 05e4bc3 Remove stray whitespace previously demanded by clang-format 3261f4d Fix help output of --generate-function-body-options 7c67b23 Merge pull request diffblue#2110 from tautschnig/type-mismatch-exception 18fb262 Merge pull request diffblue#2025 from tautschnig/stack-depth-fix 9191b6a Merge pull request diffblue#2199 from tautschnig/simplifier-typing f99e631 Merge pull request diffblue#2198 from tautschnig/fix-test-desc 1a79a11 stack depth instrumentation: __CPROVER_initialize may be empty a7690ba Merge pull request diffblue#2185 from smowton/smowton/fix/tolerate-ts18661-types fc02e8f Restore returns before writing the simplified binary 49333eb Make restore_returns handle simplified programs 46f7987 Fix perl regular expressioons in regression test descriptions 9fe432b Merge pull request diffblue#1899 from danpoe/sharing-map-catch-unit-tests 9cc6aae Merge pull request diffblue#2081 from hannes-steffenhagen-diffblue/floating_point_simplificiation da19abe Tolerate TS 18661 (_Float32 et al) types a055454 Try all rounding modes when domain is unknown 5f7bc15 Add float support to constant propagator domain 3dc2244 Move adjust_float_expressions to goto-programs 06d8bea Merge pull request diffblue#2187 from diffblue/move-convert-nondet 6d8c3fa Merge pull request diffblue#2189 from thk123/bugfix/json-parser-restart 2ad157f Merge pull request diffblue#2186 from smowton/smowton/fix/call-graph-uninit-field cd54ad7 Corrected state persistence in the json parser 4447be0 Fix uninitialised collect_callsites field in call_grapht ead0aa3 Merge pull request diffblue#2188 from smowton/smowton/fix/init-string-types-without-refine-strings 57988fc Fix String type initialisation when --refine-strings is not active 6a76aff Move convert_nondet to java_bytecode ac6eb21 Merge pull request diffblue#1858 from danpoe/dependence-graph-fix 10b8b09 Merge pull request diffblue#2011 from thomasspriggs/final_classes a154593 Merge pull request diffblue#2087 from danpoe/feature/small-map 7002909 More dependence graph tests 66263ea Make dependence graph merge() return true when abstract state changes 3aa6dca Control dependency computation fix a408423 Simplified state merging in the dependence graph 0315816 Merge pull request diffblue#2180 from thomasspriggs/json_id2string 8941567 Merge pull request diffblue#2124 from smowton/smowton/feature/fallback-function-provider cd04e70 JBMC: use simple method stubbing pass a6b2cda Add Java simple method stubbing pass ec1127c Lazy goto model: hook for driver program to replace or stub functions b6a4382 Remove `id2string` from inside calls to the `json_stringt` constructor. b673ebb Add storage of final modifier status of java classes in `java_class_typet`. a2ad909 Small map 808dade Provide suitable diagnostics for equality-without-matching-types 89cf6fe Throw appropriate exceptions when converting constraints 2ae66c2 Produce a proper error message when catching a std::runtime_error at top level e7b3ade Workaround for Visual Studio loss of CV qualifier bug 1f661f5 Move sharing map and sharing node unit tests to util 47463a3 Use std::size_t instead of unsigned in the sharing map 3e22217 Sharing map documentation e54f740 Fix sharing map compiler warnings bcc489c Move sharing map unit tests to catch 34114b8 Use a specialised endianness map for flattening git-subtree-dir: cbmc git-subtree-split: 31ef182

hannes-steffenhagen-diffblue requested review from cesaro, chrisr-diffblue, kroening, martin-cs, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners April 17, 2018 16:13

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch from 0136d94 to 801a89c Compare April 17, 2018 16:23

kroening assigned martin-cs Apr 17, 2018

peterschrammel changed the title ~~Floating point simplificiation for goto-analyzer constants domain~~ Floating point simplification for goto-analyzer constants domain Apr 17, 2018

tautschnig reviewed Apr 18, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch from 801a89c to d236828 Compare April 18, 2018 09:55

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch 5 times, most recently from 4cb6d3b to d737d60 Compare April 18, 2018 18:05

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch 3 times, most recently from b5b8986 to 3799e5d Compare April 24, 2018 12:46

NlightNFotis approved these changes Apr 25, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch from 3799e5d to b04bfd6 Compare April 26, 2018 11:54

hannes-steffenhagen-diffblue requested a review from romainbrenguier as a code owner April 26, 2018 11:54

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch 2 times, most recently from d80600f to aaf1662 Compare April 26, 2018 12:46

tautschnig reviewed May 3, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch from 9b754cd to 055e588 Compare May 4, 2018 10:36

tautschnig reviewed May 4, 2018

View reviewed changes

tautschnig approved these changes May 4, 2018

View reviewed changes

tautschnig assigned peterschrammel and chrisr-diffblue May 4, 2018

chrisr-diffblue approved these changes May 8, 2018

View reviewed changes

chrisr-diffblue removed their assignment May 8, 2018

smowton suggested changes May 14, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch from 055e588 to e0c4213 Compare May 15, 2018 12:49

smowton approved these changes May 16, 2018

View reviewed changes

tautschnig assigned hannes-steffenhagen-diffblue and unassigned peterschrammel and martin-cs May 16, 2018

hannes-steffenhagen-diffblue added 2 commits May 17, 2018 11:50

Move adjust_float_expressions to goto-programs

3dc2244

Add float support to constant propagator domain

5f7bc15

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch 2 times, most recently from d146382 to b1435ff Compare May 17, 2018 11:29

Try all rounding modes when domain is unknown

a055454

For rounding modes in constant propagator domain

hannes-steffenhagen-diffblue force-pushed the floating_point_simplificiation branch from b1435ff to a055454 Compare May 17, 2018 12:24

chrisr-diffblue merged commit 9cc6aae into diffblue:develop May 17, 2018

martin-cs reviewed May 18, 2018

View reviewed changes

chrisr-diffblue mentioned this pull request Jul 17, 2018

Regression in goto-cc since PR #2490 switch-range was merged #2583

Closed

Floating point simplification for goto-analyzer constants domain #2081

Floating point simplification for goto-analyzer constants domain #2081

Conversation

hannes-steffenhagen-diffblue commented Apr 17, 2018 • edited Loading

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue Apr 18, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig Apr 25, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue Apr 26, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented Apr 18, 2018

hannes-steffenhagen-diffblue commented Apr 18, 2018

hannes-steffenhagen-diffblue commented Apr 18, 2018 • edited Loading

NlightNFotis left a comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented May 3, 2018

tautschnig commented May 3, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented May 4, 2018

tautschnig commented May 4, 2018

hannes-steffenhagen-diffblue commented May 4, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

chrisr-diffblue left a comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented May 15, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue May 18, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue May 18, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue May 18, 2018 • edited Loading

hannes-steffenhagen-diffblue commented Apr 17, 2018 •

edited

Loading

hannes-steffenhagen-diffblue Apr 18, 2018 •

edited

Loading

tautschnig Apr 25, 2018 •

edited

Loading

hannes-steffenhagen-diffblue Apr 26, 2018 •

edited

Loading

hannes-steffenhagen-diffblue commented Apr 18, 2018 •

edited

Loading

hannes-steffenhagen-diffblue May 18, 2018 •

edited

Loading

hannes-steffenhagen-diffblue May 18, 2018 •

edited

Loading

hannes-steffenhagen-diffblue May 18, 2018 •

edited

Loading