[SV-COMP'18 12/19] SV-COMP graphml fixes [blocks: #3486] #2001

tautschnig · 2018-04-03T13:55:37Z

Do not merge as-is: this needs cleanup of patches and of the changes to expr2ct.

smowton · 2018-04-09T09:14:29Z

src/ansi-c/expr2c.cpp

@@ -699,6 +699,7 @@ std::string expr2ct::convert_struct_type(
  if(tag!="")
    dest+=" "+id2string(tag);

+#if 0


Add comment explaining why?

smowton · 2018-04-09T09:15:01Z

src/goto-programs/graphml_witness.cpp

  std::string result;

-  if(assign.rhs().id()==ID_array)
+  if(assign.rhs().id()=="array-list")


Use ID, or add one if not already present

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

src/goto-programs/graphml_witness.cpp

+    exprt clean_lhs=assign.lhs();
+    remove_l0_l1(clean_lhs);
+    std::string lhs=from_expr(ns, identifier, clean_lhs);
+    if(lhs.find("#return_value")!=std::string::npos ||


smowton · 2018-04-09T09:20:10Z

src/goto-programs/graphml_witness.cpp

+  return false;
+}
+
+static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix){


Use depth_begin et al instead of recursing?

smowton · 2018-04-09T09:21:33Z

src/goto-programs/graphml_witness.cpp

+    {
+      nodes.push_back(graphml.add_node());
+      graphml[nodes.back()].node_name="N" + std::to_string(i);
+      graphml[nodes.back()].is_violation=(i==max_thread_idx+1U) ? true : false;


I think that ternary conditional is redundant

smowton · 2018-04-09T09:21:57Z

src/goto-programs/graphml_witness.cpp

+      graphml[nodes.back()].has_invariant=false;
+    }
+
+    for(auto it=nodes.cbegin(); std::next(it)!=nodes.cend(); ++it)


INVARIANT(!nodes.empty())?

smowton · 2018-04-09T09:22:53Z

src/goto-programs/graphml_witness.cpp

+          }
+          else if(
+            id2string(it->lhs_object.get_identifier())
+              .find("#return_value")==std::string::npos &&


Several well-known identifiers to ID-ify here

smowton · 2018-04-09T09:23:15Z

src/goto-programs/graphml_witness.cpp

@@ -300,33 +428,13 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
        else if(it->type==goto_trace_stept::typet::GOTO &&
                it->pc->is_goto())
        {
+#if 0
+          // TODO: this requires knowledge about the phase of the


Provide an issue reference?

smowton · 2018-04-09T09:24:59Z

src/util/std_pair_hash.h

+inline void hash_combine(std::size_t & seed, const T & v)
+{
+  std::hash<T> hasher;
+  seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2);


Provide a reference for the particular source of magic numbers?

tautschnig · 2019-03-23T17:34:10Z

This PR is now actually ready for review. We certainly have a lot of problems left to resolve, but that would at least get develop to have the GraphML witness code that we've been using in SV-COMP the last years.

smowton · 2019-03-25T13:34:17Z

src/ansi-c/expr2c.cpp

@@ -1866,6 +1869,27 @@ std::string expr2ct::convert_constant(
      else if(dest=="-NaN")
        dest="-NAN";
    }
+    else if(dest.size() == 4 && (dest[0] == '+' || dest[0] == '-'))


Combine this and the case above to remove the redundant expression dest.size() == 4 && (dest[0] == '+' || dest[0] == '-')

I was trying to keep the diff smaller, but will now do as suggested.

smowton · 2019-03-25T13:40:44Z

src/goto-programs/graphml_witness.cpp

+namespace std // NOLINT(readability/namespace)
+{
+template <typename S, typename T>
+struct hash<pair<S, T>> // NOLINT(readability/identifiers)


Surely this belongs in util somewhere

Well, it has this single user...

smowton · 2019-03-25T13:43:55Z

src/goto-programs/graphml_witness.cpp

 std::string graphml_witnesst::convert_assign_rec(
  const irep_idt &identifier,
  const code_assignt &assign)
 {
+  static std::


Quite surprised the lifetime of this cache isn't tied to that of some class, rather than living as long as the process

I'll make it a class member.

src/goto-programs/graphml_witness.cpp

smowton · 2019-03-25T13:47:31Z

src/goto-programs/graphml_witness.cpp

+      graphml[*it].out[*std::next(it)].xml_node = edge;
+    }
+
+    // we do not provide any further details as CPAchecker does not seem to


Perhaps link to some appropriate issue or discussion thread?

A link to furious discussions at the SV-COMP meeting in Thessaloniki? :-) Or maybe sosy-lab/sv-witnesses#12?

src/goto-programs/graphml_witness.cpp

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: ee2c68b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105821202

See https://github.com/sosy-lab/sv-witnesses for the most up-to-date format specification.

https://github.com/sosy-lab/sv-witnesses documents a "control" node, and examples still include "sourcecode" nodes, but there neither is documented semantics for "control" nodes nor is it clear whether the "sourcecode" node is used by any tool.

The witness format documentation only states "Nodes where this flag is set must not have any leaving transitions" for sink nodes, but quite possibly validators expect the same for violation nodes.

NULL, NAN, INFINITY are not a keywords, just macros. Do not use them for output under the "clean" configuration.

Witness validators expect syntactically correct C code, not human-friendly pseudo-C.

Witness validators expect syntactically correct C code, and cannot cope with SSA suffixes.

The witness specification permits use of \result in assumptions (in violation witnesses), but then also requires setting assumption.resultfunction.

We must not filter out generated assertions for memory leaks.

Witness validators cannot handle array lists.

These symbols do not occur in the input program.

Witness validators cannot be expected to understand CBMC's "with" expressions. Fixes: diffblue#4486

It's actually not clear whether this is necessary or permitted, it's not contained in the official specification.

Expression-to-string conversion is costly.

This does likely need more work, but at least got us some points in the past.

@JanSvejda

We would previously use the name of the calling function. Instead, parameter assignments require a special case. Regression test kindly provided by @JanSvejda. Fixes: diffblue#4418

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 16a59aa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107154317
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

tautschnig added the do not merge label Apr 3, 2018

tautschnig requested review from kroening, peterschrammel and smowton as code owners April 3, 2018 13:55

tautschnig changed the title ~~[SV-COMP'18 11/19] SV-COMP graphml fixes~~ [SV-COMP'18 12/19] SV-COMP graphml fixes Apr 3, 2018

tautschnig self-assigned this Apr 5, 2018

smowton reviewed Apr 9, 2018

View reviewed changes

tautschnig mentioned this pull request Jul 30, 2018

Feature expr2c extension #2599

Closed

tautschnig force-pushed the sv-comp-graphml branch from c472d62 to daa0dd8 Compare November 19, 2018 17:53

tautschnig requested a review from pkesseli as a code owner November 19, 2018 17:53

tautschnig force-pushed the sv-comp-graphml branch from daa0dd8 to 917e11e Compare November 19, 2018 18:23

tautschnig requested a review from chrisr-diffblue as a code owner November 19, 2018 18:23

tautschnig mentioned this pull request Dec 1, 2018

Patch set for SV-COMP'19 [depends-on: #2000, #3462] #3486

Closed

13 tasks

tautschnig mentioned this pull request Mar 22, 2019

Witness edge scope makes name resolving ambiguous #4418

Closed

tautschnig force-pushed the sv-comp-graphml branch from 917e11e to dc199a9 Compare March 23, 2019 17:14

tautschnig added bugfix and removed do not merge labels Mar 23, 2019

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Mar 23, 2019

tautschnig force-pushed the sv-comp-graphml branch 2 times, most recently from 4fa3782 to c958e2a Compare March 23, 2019 22:37

tautschnig changed the title ~~[SV-COMP'18 12/19] SV-COMP graphml fixes~~ [SV-COMP'18 12/19] SV-COMP graphml fixes [blocks: #3486] Mar 23, 2019

tautschnig added the blocker label Mar 23, 2019

tautschnig force-pushed the sv-comp-graphml branch 2 times, most recently from ace5f4f to 808a00e Compare March 25, 2019 11:23

smowton reviewed Mar 25, 2019

View reviewed changes

tautschnig force-pushed the sv-comp-graphml branch from 808a00e to ee2c68b Compare March 26, 2019 09:40

allredj reviewed Mar 26, 2019

View reviewed changes

tautschnig mentioned this pull request Apr 4, 2019

04/2019 regression on sv-benchmarks/c/ntdrivers/cdaudio_(true|false)-unreach-call.i.cil.c #4486

Closed

peterschrammel and others added 16 commits April 4, 2019 21:23

Remove obsolete graphml frontierNode, nodeType

b231317

See https://github.com/sosy-lab/sv-witnesses for the most up-to-date format specification.

No outgoing edges from violation nodes

978e229

The witness format documentation only states "Nodes where this flag is set must not have any leaving transitions" for sink nodes, but quite possibly validators expect the same for violation nodes.

expr2ct/clean configuration: Do not output C library macros

20a816a

NULL, NAN, INFINITY are not a keywords, just macros. Do not use them for output under the "clean" configuration.

Use clean-C configuration for GraphML witnesses

0ee5675

Witness validators expect syntactically correct C code, not human-friendly pseudo-C.

Make sure SSA suffixes are stripped off GraphML output

fd27805

Witness validators expect syntactically correct C code, and cannot cope with SSA suffixes.

GraphML: Use the \result symbol in place of return value symbols

6760695

The witness specification permits use of \result in assumptions (in violation witnesses), but then also requires setting assumption.resultfunction.

Add violation node for the memory safety benchmarks

611cba2

We must not filter out generated assertions for memory leaks.

GraphML output: Split array-list into assignments

d0da778

Witness validators cannot handle array lists.

GraphML output: hide assignments to dynamic objects

0aff1c5

These symbols do not occur in the input program.

GraphML witnesses: unwind "with" expressions

6d1236d

Witness validators cannot be expected to understand CBMC's "with" expressions. Fixes: diffblue#4486

GraphML: add cyclehead node

9e303e2

It's actually not clear whether this is necessary or permitted, it's not contained in the official specification.

Using cache to speed up generation of GraphML file

3156ad7

Expression-to-string conversion is costly.

Hack to make CPAchecker parse graphml concurrency witnesses

7247f3d

This does likely need more work, but at least got us some points in the past.

GraphML witnesses: clang-format switch/case statement

a703b76

GraphML witnesses: correctly set the scope of parameters

16a59aa

We would previously use the name of the calling function. Instead, parameter assignments require a special case. Regression test kindly provided by @JanSvejda. Fixes: diffblue#4418

tautschnig force-pushed the sv-comp-graphml branch from ee2c68b to 16a59aa Compare April 4, 2019 21:24

allredj reviewed Apr 4, 2019

View reviewed changes

peterschrammel approved these changes Apr 5, 2019

View reviewed changes

tautschnig unassigned peterschrammel Apr 5, 2019

kroening approved these changes Apr 17, 2019

View reviewed changes

kroening merged commit 51e0cd7 into diffblue:develop Apr 17, 2019

tautschnig deleted the sv-comp-graphml branch April 17, 2019 12:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[SV-COMP'18 12/19] SV-COMP graphml fixes [blocks: #3486] #2001

[SV-COMP'18 12/19] SV-COMP graphml fixes [blocks: #3486] #2001

tautschnig commented Apr 3, 2018

smowton Apr 9, 2018

smowton Apr 9, 2018

smowton Apr 9, 2018

smowton Apr 9, 2018

smowton Apr 9, 2018

smowton Apr 9, 2018

smowton Apr 9, 2018

smowton Apr 9, 2018

smowton Apr 9, 2018

tautschnig commented Mar 23, 2019

smowton Mar 25, 2019

tautschnig Mar 25, 2019

smowton Mar 25, 2019

tautschnig Mar 25, 2019

smowton Mar 25, 2019

tautschnig Mar 25, 2019

smowton Mar 25, 2019

tautschnig Mar 25, 2019

allredj left a comment

allredj left a comment

[SV-COMP'18 12/19] SV-COMP graphml fixes [blocks: #3486] #2001

[SV-COMP'18 12/19] SV-COMP graphml fixes [blocks: #3486] #2001

Conversation

tautschnig commented Apr 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

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 commented Mar 23, 2019

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

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment