Well-formedness checking of SSA equation [depends on #3480] #3287

xbauch · 2018-11-07T10:13:10Z

This is an attempt at introducing well-formedness checking into SSA equation. It follows the process of #3123 by implementing the validate method in SSA_stept and extending ssa_exprt with check/validate functionality. Unit tests will be included if the attempt is deemed worthy of pursuing.

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.
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.

danpoe

Looks good so far, a few minor comments

danpoe · 2018-11-07T19:15:22Z

src/cbmc/cbmc_parse_options.cpp

+  if(cmdline.isset("validate-ssa-equation"))
+  {
+    options.set_option("validate-ssa-equation", true);
+  }


This should best be put in cbmc_parse_optionst::get_command_line_options()

danpoe · 2018-11-07T19:22:29Z

src/util/ssa_expr.h

+    DATA_CHECK(!has_operands(), "SSA expression do not have operands");
+    DATA_CHECK(id() == ID_symbol, "SSA expression symbols are symbols");
+    DATA_CHECK(get_bool(ID_C_SSA_symbol), "wrong SSA expression ID");
+  }


Btw, these methods have now become static methods that take the parent type in the recent changes to PR #3123. So that would then become static void check(const exprt &expr, const validation_modet vm).

We should also add a case for SSA_exprt to call_on_expr() in validate_expressions.cpp.

danpoe · 2018-11-07T19:30:25Z

src/util/ssa_expr.h

+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(!has_operands(), "SSA expression do not have operands");


Nit: According to the coding standard (cbmc/CODING_STANDARD.md), if possible the messages in invariants should be "should" statements that describe what should hold, e.g. "SSA expression should have operands".

peterschrammel · 2018-11-07T21:10:54Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -125,8 +125,29 @@ int goto_instrument_parse_optionst::doit()

    get_goto_program();

+    {
+      const bool b = cmdline.isset("validate-goto-binary");


What does b stand for?

peterschrammel · 2018-11-07T21:11:55Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1572,6 +1593,12 @@ void goto_instrument_parse_optionst::help()
    " --show-local-safe-pointers   show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
    " --show-safe-dereferences     show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
    "                              *and* used as a dereference operand\n" // NOLINT(*)
+    // NOLINTNEXTLINE(whitespace/line_length)


I suggest to provide HELP_VALIDATION and OPT_VALIDATION to avoid code duplication.

peterschrammel · 2018-11-07T21:16:12Z

src/util/validate.h

+  }
+};
+
+#endif /* CPROVER_UTIL_VALIDATE_H */


// preferred

peterschrammel · 2018-11-07T21:16:22Z

src/util/validate_code.h

+  const namespacet &ns,
+  const validation_modet vm);
+
+#endif /* CPROVER_UTIL_VALIDATE_CODE_H */


// preferred

peterschrammel · 2018-11-07T21:16:55Z

src/util/validate_expressions.h

+  const namespacet &ns,
+  const validation_modet vm);
+
+#endif /* CPROVER_UTIL_VALIDATE_EXPRESSIONS_H */


// preferred

peterschrammel · 2018-11-07T21:17:47Z

src/util/validate_types.h

+  const namespacet &ns,
+  const validation_modet vm);
+
+#endif /* CPROVER_UTIL_VALIDATE_TYPES_H */


// preferred

peterschrammel · 2018-11-07T21:18:34Z

src/util/validate_types.h

+class namespacet;
+enum class validation_modet;
+
+void check_type_pick(const typet &type, const validation_modet vm);


Parameter names could be omitted in the declarations. It's obvious what they are.

martin-cs · 2018-11-07T21:19:11Z

src/cbmc/cbmc_parse_options.cpp

+  {
+    const namespacet ns(goto_model.symbol_table);
+    goto_model.validate(ns, validation_modet::INVARIANT);
+  }


Is this from a previous PR as it doesn't match the description of the PR?

martin-cs · 2018-11-07T21:21:06Z

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -406,6 +406,12 @@ int goto_analyzer_parse_optionst::doit()
  if(process_goto_program(options))
    return CPROVER_EXIT_INTERNAL_ERROR;

+  if(cmdline.isset("validate-goto-model"))
+  {


So, I'm opinionated but ... why add this option to every program? Why not just add it to goto-instrument? If it's the same check (and eventually everyone will do it on program load) why do we need the extra option everywhere?

xbauch · 2018-11-09T09:42:51Z

Rebased onto #3123 branch to follow the latest version. Only the last commit pertain to SSA checking. Once #3123 is merged into develop, this will be rebased onto that and hopefully cleaner.

tautschnig

Some comments below, but the biggest item that I'd like to see added/changed is the current check_renaming of goto_symex_state.cpp to be moved into the validation framework and thus only done when validation is enabled.

src/cbmc/bmc.cpp

tautschnig · 2018-11-14T11:49:55Z

src/goto-symex/symex_target_equation.cpp

+    validate_full_expr(ssa_full_lhs, ns, vm);
+    validate_full_expr(original_full_lhs, ns, vm);
+    validate_full_expr(ssa_rhs, ns, vm);
+    base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns);


This has no effect?

Oh, my bad: this was intended to check that lhs and rhs have the same type. Should be fixed now.

src/goto-symex/symex_target_equation.cpp

allredj

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

xbauch · 2018-11-15T09:24:42Z

@tautschnig regarding the check_renaming: I've tried moving this check into the validation framework. I ended up adding a validation_modet variable to both goto_symext and goto_symex_statet and an IGNORE validation mode. Have a look if this is what you had in mind.

tautschnig · 2018-11-15T09:36:08Z

src/goto-symex/goto_symex.h

@@ -76,7 +76,8 @@ class goto_symext
      path_storage(path_storage),
      path_segment_vccs(0),
      _total_vccs(std::numeric_limits<unsigned>::max()),
-      _remaining_vccs(std::numeric_limits<unsigned>::max())
+      _remaining_vccs(std::numeric_limits<unsigned>::max()),
+      global_validation_mode(validation_modet::IGNORE)


Wouldn't it be possible to look at options instead and store that in a Boolean, as is done for several other entries in options above?

Well I can use options in goto_symext but not in statet (unless I pass it there somehow).

tautschnig · 2018-11-15T09:38:35Z

src/goto-symex/goto_symex_state.cpp

@@ -241,9 +217,10 @@ void goto_symex_statet::assignment(
  // the type might need renaming
  rename(lhs.type(), l1_identifier, ns);
  lhs.update_type();
-  assert_l1_renaming(lhs);
+  const validation_modet vm = global_validation_mode;
+  DATA_CHECK(!check_renaming_l1(lhs), "lhs renaming failed on l1");


What I'd do here is something along the lines of !validation_enabled || !check_renaming_l1(lhs) to avoid changing the validation_modet enum.

I reverted the new validation mode. I'm not sure if you're suggesting not to use DATA_CHECK at all and just call the regular invariants, or not. Have a look at the new version.

tautschnig

Many thanks for the update!

tautschnig · 2018-11-15T14:08:19Z

src/goto-symex/goto_symex.h

@@ -524,7 +524,7 @@ class goto_symext
  {
    target.validate(ns, vm);
  }
-  validation_modet global_validation_mode;
+  bool run_validation_checks;


With the exception that I'd place this textually next to the other Boolean variables that store options, yes, this is how I thought it could be done.

tautschnig · 2018-11-15T14:09:28Z

src/goto-symex/goto_symex_state.cpp

+  if(run_validation_checks)
+  {
+    const validation_modet vm = local_validation_mode;
+    DATA_CHECK(!check_renaming_l1(lhs), "lhs renaming failed on l1");


Hopefully that pain will go away soon when DATA_CHECK takes three arguments...

tautschnig · 2018-11-15T14:11:17Z

src/goto-symex/symex_main.cpp

@@ -301,7 +301,7 @@ void goto_symext::symex_from_entry_point_of(

  statet state;

-  state.global_validation_mode = global_validation_mode;
+  state.run_validation_checks = run_validation_checks;


One future day we will actually have a proper constructor I suppose...

allredj

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

xbauch · 2018-11-16T16:49:44Z

@tautschnig I've moved the Boolean flag to the previous ones and squashed the commits.

allredj

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

chrisr-diffblue

LGTM, but would be good to rebase on top of #3480 and make the implicit parameter to DATA_CHECK be explicit.

danpoe · 2018-11-29T16:43:51Z

src/goto-symex/goto_symex_state.cpp

-  assert_l1_renaming(lhs);
-
-  #if 0
+  const validation_modet local_validation_mode = validation_modet::INVARIANT;


If the validation mode is hardcoded to validation_modet::INVARIANT we could also use DATA_INVARIANT() directly instead. I think when using DATA_CHECK() the mode should be truly configurable.

danpoe · 2018-11-29T16:54:43Z

unit/goto-symex/ssa_equation.cpp

+        {
+          caught = true;
+        }
+        REQUIRE(caught);


I think catch supports REQUIRE_THROWS_* macros to check that a particular exception is thrown.

Follows the diffblue#3123 skeleton with additional checks in SSA_stept. Adds a condition such that renaming checks are only run with the validate option.

allredj

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

…plicit-argument Make validation mode parameter explicit in DATA_CHECK macros [blocks #3287]

xbauch added the do not merge label Nov 7, 2018

xbauch requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners November 7, 2018 10:13

xbauch changed the title ~~Feature/ssa validate~~ Well-formedness checking of SSA equation Nov 7, 2018

danpoe reviewed Nov 7, 2018

View reviewed changes

peterschrammel reviewed Nov 7, 2018

View reviewed changes

martin-cs reviewed Nov 7, 2018

View reviewed changes

xbauch force-pushed the feature/ssa_validate branch from 4c66ee5 to e5349cc Compare November 9, 2018 09:35

xbauch requested review from cesaro, cristina-david, forejtv, NathanJPhillips, romainbrenguier and thk123 as code owners November 9, 2018 09:35

xbauch force-pushed the feature/ssa_validate branch from e5349cc to 971df90 Compare November 9, 2018 11:09

tautschnig assigned xbauch Nov 10, 2018

xbauch force-pushed the feature/ssa_validate branch from 971df90 to ea8c694 Compare November 14, 2018 10:32

xbauch removed the do not merge label Nov 14, 2018

tautschnig reviewed Nov 14, 2018

View reviewed changes

allredj reviewed Nov 14, 2018

View reviewed changes

tautschnig reviewed Nov 15, 2018

View reviewed changes

allredj reviewed Nov 16, 2018

View reviewed changes

xbauch force-pushed the feature/ssa_validate branch from 77868dc to 6bc7648 Compare November 16, 2018 16:47

xbauch force-pushed the feature/ssa_validate branch from 6bc7648 to 242655b Compare November 16, 2018 16:56

allredj reviewed Nov 16, 2018

View reviewed changes

xbauch assigned tautschnig and unassigned xbauch Nov 19, 2018

johnnonweiler assigned danpoe Nov 29, 2018

chrisr-diffblue changed the title ~~Well-formedness checking of SSA equation~~ Well-formedness checking of SSA equation [depends on #3480] Nov 29, 2018

chrisr-diffblue approved these changes Nov 29, 2018

View reviewed changes

danpoe approved these changes Nov 29, 2018

View reviewed changes

danpoe and others added 2 commits November 30, 2018 08:25

Make validation mode parameter explicit in DATA_CHECK() macros

7429ac8

Well-formedness checking for SSA

eb0b86b

Follows the diffblue#3123 skeleton with additional checks in SSA_stept. Adds a condition such that renaming checks are only run with the validate option.

xbauch force-pushed the feature/ssa_validate branch from 242655b to eb0b86b Compare November 30, 2018 10:55

xbauch unassigned danpoe Nov 30, 2018

allredj reviewed Nov 30, 2018

View reviewed changes

tautschnig added a commit that referenced this pull request Dec 1, 2018

Merge pull request #3480 from danpoe/refactor/make-validation-mode-ex…

e62a14c

…plicit-argument Make validation mode parameter explicit in DATA_CHECK macros [blocks #3287]

tautschnig approved these changes Dec 1, 2018

View reviewed changes

tautschnig merged commit a6e0660 into diffblue:develop Dec 1, 2018

tautschnig mentioned this pull request Dec 1, 2018

[SV-COMP'18 2/19] Do not perform SSA sanity checks #1991

Closed

xbauch deleted the feature/ssa_validate branch December 4, 2018 08:57

Well-formedness checking of SSA equation [depends on #3480] #3287

Well-formedness checking of SSA equation [depends on #3480] #3287

Conversation

xbauch commented Nov 7, 2018

danpoe 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

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

xbauch commented Nov 9, 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

allredj left a comment

Choose a reason for hiding this comment

xbauch commented Nov 15, 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

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

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

xbauch commented Nov 16, 2018

allredj left a comment

Choose a reason for hiding this comment

chrisr-diffblue left a 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

xbauch commented Nov 9, 2018 •

edited

Loading