Output C code from harness generation tool. #5343

NlightNFotis · 2020-05-14T13:56:10Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

hannes-steffenhagen-diffblue · 2020-05-14T13:59:48Z

regression/goto-harness/havoc-global-int-02/main.c

@@ -3,7 +3,7 @@
 unsigned int x;
 unsigned int y;

-unsigned int nondet_int()
+unsigned int some_random_unsigned_integer()


This was changed because of a dump_c() bug; It assumes that nondet_* names are available with specific meanings.

hannes-steffenhagen-diffblue · 2020-05-14T14:01:10Z

regression/goto-harness/havoc-global-int-02/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG


We can work around this for now by re-enabling the old behaviour for these, but we've marked them KNOWNBUG for now because we're first trying to get the call-function harness to behave like we want it to.

hannes-steffenhagen-diffblue · 2020-05-20T14:33:59Z

src/goto-harness/Makefile

+  ../ansi-c/ansi-c$(LIBEXT) \
+  ../cpp/cpp$(LIBEXT) \
+  ../goto-instrument/dump_c$(OBJEXT) \
+  ../goto-instrument/goto_program2code$(OBJEXT) \


these are all needed for dump_c

Previously the `dump-c` output of recursive initialisation wouldn't work with types that have nested const things in them, such as pointer-to-const or array with constant elements.

codecov · 2020-05-20T16:44:44Z

Codecov Report

Merging #5343 into develop will decrease coverage by 0.09%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #5343      +/-   ##
===========================================
- Coverage    68.16%   68.07%   -0.10%     
===========================================
  Files         1170     1170              
  Lines        96441    96477      +36     
===========================================
- Hits         65735    65672      -63     
- Misses       30706    30805      +99

Flag	Coverage Δ
#cproversmt2	`42.47% <0.00%> (-0.01%)`	⬇️
#regression	`65.29% <100.00%> (-0.08%)`	⬇️
#unit	`31.76% <0.00%> (-0.01%)`	⬇️

Impacted Files	Coverage Δ
src/util/type.h	`100.00% <ø> (ø)`
...c/goto-harness/function_call_harness_generator.cpp	`80.23% <100.00%> (ø)`
src/goto-harness/goto_harness_parse_options.cpp	`77.77% <100.00%> (+7.77%)`	⬆️
...goto-harness/memory_snapshot_harness_generator.cpp	`61.87% <100.00%> (-26.52%)`	⬇️
src/goto-harness/recursive_initialization.cpp	`87.14% <100.00%> (+0.58%)`	⬆️
src/goto-harness/recursive_initialization.h	`100.00% <100.00%> (ø)`
src/util/type.cpp	`71.42% <100.00%> (+21.42%)`	⬆️
...c/goto-harness/memory_snapshot_harness_generator.h	`71.05% <0.00%> (-26.32%)`	⬇️
src/memory-analyzer/analyze_symbol.cpp	`72.81% <0.00%> (-18.13%)`	⬇️
... and 7 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update f20278a...d8a9207. Read the comment docs.

The C output doesn't quite work with the snapshot harness at the moment (specifically, it doesn't work with the feature to restart analysis from a specific point in the program) so these test are marked as KNOWNBUG for now. Going forward we may re-enable these after fixing the feature, or possibly do without the restarting entirely.

Modify goto-harness to output C code that corresponds to the added harness functions and some global values. This has been a feature request.

danpoe

LGTM

chrisr-diffblue

Mostly looks OK, but a couple of queries I'd like answered if possible?

chrisr-diffblue · 2020-05-28T12:10:48Z

src/goto-harness/recursive_initialization.h

@@ -22,6 +22,7 @@ Author: Diffblue Ltd.
 #include "function_harness_generator_options.h"
 #include "goto_harness_generator.h"

+#define GOTO_HARNESS_PREFIX "GOTO_HARNESS"


I would have thought that as this is an "implementation" prefix, it should be __GOTO_HARNESS ? (i.e. double underscore at the front) ?

chrisr-diffblue · 2020-05-28T12:11:57Z

src/util/type.cpp

@@ -28,3 +28,9 @@ void type_with_subtypest::move_to_subtypes(typet &type)
  sub.push_back(static_cast<const typet &>(get_nil_irep()));
  sub.back().swap(type);
 }
+
+typet remove_const(typet type)


const argument? Or if this is modifying the argument, then why return ?

It's returning a copy with the modification. If the argument was const we'd have to make two copies, if it was const reference we'd still have to make a copy so we don't gain anything in either case.

OK, I like the const just to make it explicit - and of course depending on how much this is called, an extra copy probably isn't the end of the world... But its a nitpick really on my part.

chrisr-diffblue · 2020-05-28T12:14:33Z

src/util/type.h

@@ -224,4 +224,8 @@ inline type_with_subtypest &to_type_with_subtypes(typet &type)
    for(type_with_subtypest::subtypest::iterator it=to_type_with_subtypes(type).subtypes().begin(); \
        it!=to_type_with_subtypes(type).subtypes().end(); ++it)

+/// Remove const qualifier from type (if any).
+/// Returns type as is if there is no const qualifier.
+typet remove_const(typet type);


Yeah, I'm not sure why this is a member function rather than a static?

Before this change, we were using CPROVER_PREFIX, which was causing some symbols to be dropped before the C code output because of the prefix symbolising CProver internal values.

chrisr-diffblue

LGTM

smowton

Seems ok except the hundred or so tests that get marked KNOWNBUG here -- what was the memory-snapshot thingy that got trashed?

smowton · 2020-05-28T15:10:26Z

src/goto-harness/recursive_initialization.cpp

+      if(component.type().get_bool(ID_C_constant))
+      {
+        return dereference_exprt{
+          typecast_exprt{address_of_exprt{std::move(member_expr)},


Comment that this pile of stuff amounts to *(X*)&field, where field has type const X*

Also I take it you've tried using braced initialiser style for such things?

smowton · 2020-05-28T15:14:25Z

src/Makefile

       goto-instrument \
+       goto-harness \


Sort order was correct before

NlightNFotis · 2020-05-28T21:08:26Z

@smowton We are tracking the broken tests internally and through github issue #5351. The memory snapshot harness was one of the modes that the goto-harness tool supported.

NlightNFotis requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners May 14, 2020 13:56

NlightNFotis added the do not review label May 14, 2020

hannes-steffenhagen-diffblue marked this pull request as draft May 14, 2020 13:57

hannes-steffenhagen-diffblue reviewed May 14, 2020

View reviewed changes

NlightNFotis force-pushed the feature/harness_dirty branch 17 times, most recently from 65b63fe to aa7d1d9 Compare May 19, 2020 10:54

hannes-steffenhagen-diffblue reviewed May 20, 2020

View reviewed changes

NlightNFotis mentioned this pull request May 20, 2020

Memory Snapshot Harness tests are marked KnownBug #5351

Closed

NlightNFotis force-pushed the feature/harness_dirty branch 2 times, most recently from 205327f to 46f8a54 Compare May 20, 2020 15:37

hannes-steffenhagen-diffblue and others added 2 commits May 20, 2020 17:11

Initialise const values recursively.

feb3f50

Previously the `dump-c` output of recursive initialisation wouldn't work with types that have nested const things in them, such as pointer-to-const or array with constant elements.

Add missing local declaration in recursive_initialization.cpp

cf69bd5

NlightNFotis force-pushed the feature/harness_dirty branch from 46f8a54 to 881125f Compare May 20, 2020 16:11

NlightNFotis force-pushed the feature/harness_dirty branch from 43e4a83 to e5114db Compare May 21, 2020 15:00

NlightNFotis added 5 commits May 22, 2020 10:10

Output C code instead of goto-binary from goto-harness.

431df6a

Modify goto-harness to output C code that corresponds to the added harness functions and some global values. This has been a feature request.

Remove unneeded parameter from get_fresh_local_typed_symexpr.

26e534c

Add mode to get_fresh_local_typed_symexpr

bfea4e6

Add flags to objects created by get_fresh_global_symbol.

17f3c79

NlightNFotis force-pushed the feature/harness_dirty branch from e5114db to d404ae1 Compare May 22, 2020 09:10

NlightNFotis marked this pull request as ready for review May 22, 2020 09:10

NlightNFotis marked this pull request as ready for review May 22, 2020 09:34

NlightNFotis changed the title ~~Feature/harness dirty~~ Output C code from harness generation tool. May 26, 2020

hannes-steffenhagen-diffblue removed the do not review label May 26, 2020

danpoe approved these changes May 26, 2020

View reviewed changes

hannes-steffenhagen-diffblue approved these changes May 28, 2020

View reviewed changes

chrisr-diffblue reviewed May 28, 2020

View reviewed changes

NlightNFotis added 3 commits May 28, 2020 14:44

Add GOTO_HARNESS_PREFIX.

4b1151c

Before this change, we were using CPROVER_PREFIX, which was causing some symbols to be dropped before the C code output because of the prefix symbolising CProver internal values.

Make is_initialization_allowed static and change init conditions.

f8a6c91

Add mode to param symbol in recursive initialization

d8a9207

NlightNFotis force-pushed the feature/harness_dirty branch from d404ae1 to d8a9207 Compare May 28, 2020 13:46

chrisr-diffblue approved these changes May 28, 2020

View reviewed changes

smowton approved these changes May 28, 2020

View reviewed changes

NlightNFotis merged commit 87ee713 into diffblue:develop May 28, 2020

Output C code from harness generation tool. #5343

Output C code from harness generation tool. #5343

Uh oh!

Conversation

NlightNFotis commented May 14, 2020

Uh oh!

hannes-steffenhagen-diffblue May 14, 2020 • edited by NlightNFotis 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!

codecov bot commented May 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

danpoe left a comment

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue 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!

hannes-steffenhagen-diffblue May 28, 2020 • 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!

chrisr-diffblue left a comment

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented May 28, 2020

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue May 14, 2020 •

edited by NlightNFotis

Loading

codecov bot commented May 20, 2020 •

edited

Loading

hannes-steffenhagen-diffblue May 28, 2020 •

edited

Loading