Support for explicit sliceable assumes

[rafaelsamenezes]

Closes #1634

This adds the concept of an sliceable assumption, which differs from the common assumptions as it is an invariant instead of a precondition. This mostly affects the Interval Analysis (specially the more aggressive instrumentation modes) as adding complex invariants made the program difficult to slice. This results in the invariant assumption affecting falsification of programs, leading us to use weaker instrumentations mode (i.e., guard local).

Master - 120s, Action 797

Statistics:           9537 Files
  correct:            4259
    correct true:     2657
    correct false:    1602
  incorrect:             6
    incorrect true:      6
    incorrect false:     0
  unknown:            5272
  Score:              6724 (max: 15923)

PR - 120s, Action 809

Statistics:           9537 Files
  correct:            4288
    correct true:     2669
    correct false:    1619
  incorrect:             6
    incorrect true:      6
    incorrect false:     0
  unknown:            5243
  Score:              6765 (max: 15923)

[lucasccordeiro]

LGTM.

[fbrausse]

In general looks fine, but I have a couple of comments.

1. I think there is a discrepancy for the defaults assigned to sliceable.

   • instructiont::clear() sets it to false, same as the constructor of that class.
   • SSA_stept constructor sets it to false as well, so that's consistent.

   But:

   • do_function_call_symbol() sets the flag to true for only certain assumptions, in particular, assertions will get sliceable == false.
   • symex_target_equationt::assertion() sets the flag to true for ASSERT SSA-steps.

   As setting this flag to true is an opt-out of the default (--slice-assumes not given on the cmdline), I believe symex_target_equationt::assertion() should not set it to true.

2. What does sliceable == false actually mean for both, instructiont and SSA_stept? For assumptions: nothing, use the default, which is that assumptions are not sliced. For any other kind of statement it has no influence on the operation. But this is not intuitive with the default value false: The slicer does operate on these other kinds of statements, so the default should be true.

3. Also, I feel that instructiont::make_assumption() should get this new flag as a parameter.

[fbrausse]

The comment here should state that this flag is only relevant for assumptions.

[fbrausse]

PS: I might have stated points 1. and 2. clearer, as they might read contradictory. What I meant: maybe this flag should be called unsliceable (or no_slice, in analogy to the --no-slice* options) and default to true for assumptions (except the new one) and to false for all other kinds of (sliceable) statements.

[rafaelsamenezes]

PS: I might have stated points 1. and 2. clearer, as they might read contradictory. What I meant: maybe this flag should be called unsliceable (or no_slice, in analogy to the --no-slice* options) and default to true for assumptions (except the new one) and to false for all other kinds of (sliceable) statements.

I see your point. I think that the confusion will happen due to the flag not having an explicit relation with assumptions. I guess we could rename it to sliceable_assumption. IMO renaming it to unsliceable will lead to the same confusion, unless we extend this concept for all instructions (with everything except assume/assert being sliceable by default).

[fbrausse]

due to the flag not having an explicit relation with assumptions

Should it? We could make it more general in the future, that's why the default should match the current semantics for all instruction/SSA-step types and a comment could mention that the implementation currently just supports ASSUME.

[rafaelsamenezes]

We could make it more general in the future

Then I feel like the correct approach is to keep sliceable and set it to true for every instruction except asserts/assumes and then add a check for it in every step for the slicer. The slice assumes option should then just affect the initialization of the sliceable attribute.

[fbrausse]

Then I feel like the correct approach is to keep sliceable and set it to true for every instruction except asserts/assumes and then add a check for it in every step for the slicer. The slice assumes option should then just affect the initialization of the sliceable attribute.

I agree.

[rafaelsamenezes]

I moved to draft while I fix the latest changes

Statistics:           9537 Files
  correct:            4259
    correct true:     2655
    correct false:    1604
  incorrect:             7
    incorrect true:      6
    incorrect false:     1
  unknown:            5271
  Score:              6706 (max: 15923)

[rafaelsamenezes]

Hm apparently, the issue is that this constructor is being used and manipulated without a proper call to make_assume:

    inline instructiont()
      : location(static_cast<const locationt &>(get_nil_irep())),
        type(NO_INSTRUCTION_TYPE),
        inductive_step_instruction(false),
        inductive_assertion(false),
        location_number(0),
        loop_number(unsigned(0)),
        target_number(unsigned(-1))
    {
      guard = gen_true_expr();
    }

[rafaelsamenezes]

Latest version:

Statistics:           9537 Files
  correct:            4261
    correct true:     2656
    correct false:    1605
  incorrect:             6
    incorrect true:      6
    incorrect false:     0
  unknown:            5270
  Score:              6725 (max: 15923)

@fbrausse it seems that the instruction in ESBMC are quite inconsistent. May I revert back the latest changes?

[fbrausse]

Latest version:

Statistics:           9537 Files
  correct:            4261
    correct true:     2656
    correct false:    1605
  incorrect:             6
    incorrect true:      6
    incorrect false:     0
  unknown:            5270
  Score:              6725 (max: 15923)

@fbrausse it seems that the instruction in ESBMC are quite inconsistent. May I revert back the latest changes?

The score changes aren't huge. Keep in mind that the current sv-comp runs are also less stable. Having said that, I would prefer to have consistent defaults. Appearently with the current modification patterns of instructions it's hard to do, so I'm fine with going back to "the inconsistent default", though maybe it's best to take a look at the actual diff of the sv-comp results before that - just so we know we're not chasing noise.