Xml description addition #6237

TGWDB · 2021-07-20T10:12:03Z

This unifies the XML output with the JSON output by including the description in XML.

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.

This unifies XML output with JSON output for results by also outputting the "description" in the XML. Fixes diffblue#3798

Fix regression test that matches on XML output, now includes description..

martin-cs

In principle, seems like a good idea to be consistent and that this is useful information. However, we do need to be careful with output formats, esp. machine readable ones. I think this should be backwards compatible though.

This updates the XML schema that is used to validate XML output to now allow desciption in result output.

This skips two tests that use characters for operators where the character cannot be printed in XML

This adds a KNOWNBUG regression test for printing special operators in traces. This is also a bug in XML output but not JSON.

TGWDB · 2021-07-20T13:32:43Z

I recommend reviewing by commit, each is quite straightforward but do different things.

codecov · 2021-07-20T14:46:58Z

Codecov Report

Merging #6237 (cb2457b) into develop (db1a8b0) will decrease coverage by 0.00%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #6237      +/-   ##
===========================================
- Coverage    75.47%   75.47%   -0.01%     
===========================================
  Files         1459     1463       +4     
  Lines       161447   161246     -201     
===========================================
- Hits        121852   121699     -153     
+ Misses       39595    39547      -48

Impacted Files	Coverage Δ
src/goto-checker/properties.cpp	`74.56% <100.00%> (+0.22%)`	⬆️
src/ansi-c/ansi_c_convert_type.cpp	`73.03% <0.00%> (-6.21%)`	⬇️
src/util/simplify_expr_boolean.cpp	`86.11% <0.00%> (-2.78%)`	⬇️
src/util/c_types.h	`99.11% <0.00%> (-0.89%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`60.89% <0.00%> (-0.67%)`	⬇️
src/util/simplify_expr.cpp	`78.22% <0.00%> (-0.31%)`	⬇️
src/goto-instrument/code_contracts.cpp
src/goto-instrument/code_contracts.h
...rc/goto-instrument/contracts/memory_predicates.cpp	`84.00% <0.00%> (ø)`
src/goto-instrument/contracts/contracts.cpp	`92.04% <0.00%> (ø)`
... 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 06c563a...cb2457b. Read the comment docs.

NlightNFotis · 2021-07-20T14:54:19Z

regression/cbmc/ACSL/fail-operators.c

+  __CPROVER_bool a, b;
+  __CPROVER_assert(!(a ≡ b) == (a == b), "≥");
+  __CPROVER_assert(!(a ≢ b) == (a != b), "≢");
+  __CPROVER_assert(!(a ⇒ b) == (!a || b), "⇒");


These looked a bit suspicious to me, but it looks like the C Compiler (or at least, GCC does) determines file encoding from reading the file, defaulting to either ASCII or UTF-8, and we are using ifstream to read files, which has its encoding information set through std::locale, so it looks like this should work.

thomasspriggs · 2021-07-21T09:32:38Z

regression/validate-trace-xml-schema/check.py

-    ['String_Abstraction17', 'test.desc']
+    ['String_Abstraction17', 'test.desc'],
+    # these tests use characters that cannot be displayed in XML
+    ['ACSL', 'operators.desc'],


🚫 If the changes cause output to include more characters that are invalid XML then they should not be merged. The correct thing to do would be to escape these characters.

For details of how escaping works in XML see - https://www.w3.org/TR/REC-xml/#syntax
I think the code for this escaping exists already. See xmlt::escape_attribute in src/util/xml.cpp.

☝️ What he said. Let's not generate invalid XML.

tautschnig · 2021-08-13T09:55:46Z

regression/cbmc/xml-interface1/test.desc

-<result property="foo\.assertion\.3" status="SUCCESS"/>
-<result property="foo\.assertion\.1" status="FAILURE">
+<result description="assertion 0" property="foo\.assertion\.3" status="SUCCESS"/>
+<result description="assertion 0" property="foo\.assertion\.1" status="FAILURE">


Nit pick: I'd prefer for this commit to be merged with prior commit that causes this test to break. Just makes any future bisecting easier.

tautschnig · 2021-08-13T09:56:12Z

doc/assets/xml_spec.xsd

@@ -166,6 +166,7 @@
      <xs:sequence>
        <xs:element ref="goto_trace" minOccurs="0"/>
      </xs:sequence>
+      <xs:attribute name="description" type="xs:string"/>


This one should also be merged with the code change.

tautschnig · 2021-08-13T09:58:37Z

regression/cbmc/ACSL/fail-operators.desc

+The verification should fail. Note that this is a bug for normal
+and XML output, but not JSON.


It's not really clear to me what is failing here: is the actual verification outcome wrong just because of special characters?! Or is there just some issue with the output?

TGWDB added 2 commits July 20, 2021 11:08

Output description in XML

4c06afa

This unifies XML output with JSON output for results by also outputting the "description" in the XML. Fixes diffblue#3798

Fix regression test using XML output

0b88930

Fix regression test that matches on XML output, now includes description..

TGWDB requested review from kroening, peterschrammel and tautschnig as code owners July 20, 2021 10:12

martin-cs approved these changes Jul 20, 2021

View reviewed changes

TGWDB added 2 commits July 20, 2021 13:57

Update XML schema to allow description in results

624743d

This updates the XML schema that is used to validate XML output to now allow desciption in result output.

Skip tests that display unprintable characters in XML

6f521a4

This skips two tests that use characters for operators where the character cannot be printed in XML

TGWDB requested a review from chrisr-diffblue as a code owner July 20, 2021 12:58

Add KNOWNBUG regression test for printing special operators

cb2457b

This adds a KNOWNBUG regression test for printing special operators in traces. This is also a bug in XML output but not JSON.

NlightNFotis approved these changes Jul 20, 2021

View reviewed changes

chrisr-diffblue approved these changes Jul 20, 2021

View reviewed changes

thomasspriggs suggested changes Jul 21, 2021

View reviewed changes

tautschnig assigned TGWDB Aug 11, 2021

tautschnig reviewed Aug 13, 2021

View reviewed changes

TGWDB closed this Oct 11, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Xml description addition #6237

Xml description addition #6237

TGWDB commented Jul 20, 2021 •

edited

Loading

martin-cs left a comment

TGWDB commented Jul 20, 2021

codecov bot commented Jul 20, 2021 •

edited

Loading

NlightNFotis Jul 20, 2021

thomasspriggs Jul 21, 2021

thomasspriggs Jul 21, 2021

martin-cs Jul 21, 2021

tautschnig Aug 13, 2021

tautschnig Aug 13, 2021

tautschnig Aug 13, 2021

		The verification should fail. Note that this is a bug for normal
		and XML output, but not JSON.

Xml description addition #6237

Xml description addition #6237

Conversation

TGWDB commented Jul 20, 2021 • edited Loading

martin-cs left a comment

Choose a reason for hiding this comment

TGWDB commented Jul 20, 2021

codecov bot commented Jul 20, 2021 • edited Loading

Codecov Report

NlightNFotis Jul 20, 2021

Choose a reason for hiding this comment

thomasspriggs Jul 21, 2021

Choose a reason for hiding this comment

thomasspriggs Jul 21, 2021

Choose a reason for hiding this comment

martin-cs Jul 21, 2021

Choose a reason for hiding this comment

tautschnig Aug 13, 2021

Choose a reason for hiding this comment

tautschnig Aug 13, 2021

Choose a reason for hiding this comment

tautschnig Aug 13, 2021

Choose a reason for hiding this comment

TGWDB commented Jul 20, 2021 •

edited

Loading

codecov bot commented Jul 20, 2021 •

edited

Loading