Skip checking frame conditions for local variables

[feliperodri]

Resolves #6154

It avoids unnecessary assertions (improving performance) and it prevents cases where memory primitives are invoked with dead objects.

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

[codecov]

Codecov Report

Merging #6279 (c305f90) into develop (645c07b) will increase coverage by 0.06%.
The diff coverage is 96.98%.

@@             Coverage Diff             @@
##           develop    #6279      +/-   ##
===========================================
+ Coverage    75.90%   75.97%   +0.06%     
===========================================
  Files         1492     1503      +11     
  Lines       162714   163159     +445     
===========================================
+ Hits        123511   123962     +451     
+ Misses       39203    39197       -6     

Impacted Files	Coverage Δ
...alyses/variable-sensitivity/abstract_environment.h	100.00% <ø> (ø)
...rc/analyses/variable-sensitivity/abstract_object.h	76.92% <ø> (ø)
...ses/variable-sensitivity/constant_abstract_value.h	100.00% <ø> (ø)
...ble-sensitivity/constant_pointer_abstract_object.h	100.00% <ø> (ø)
...ses/variable-sensitivity/context_abstract_object.h	85.71% <ø> (ø)
.../variable-sensitivity/full_array_abstract_object.h	100.00% <ø> (ø)
...variable-sensitivity/full_struct_abstract_object.h	100.00% <ø> (ø)
...ses/variable-sensitivity/interval_abstract_value.h	100.00% <ø> (ø)
...s/variable-sensitivity/value_set_abstract_object.h	100.00% <ø> (ø)
...le-sensitivity/value_set_pointer_abstract_object.h	100.00% <ø> (ø)
... and 64 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 b60259a...c305f90. Read the comment docs.

[SaswatPadhi]

Just one comment below.

Other than that, can we add a test case where we assign to a local variable with the same name as the global variable and make sure that things work correctly? Something like:

int x;
void pure()
__CPROVER_assigns()
{
  int x;
  x++;
}

[SaswatPadhi]

I think this would make it impossible to test certain behaviors on invalid pointers. Can we add this to the specific test that requires it? We can do so by adding _ --pointer-primitive-check to the list of flags (note the underscore). For example:

cbmc/regression/contracts/variant_init_inside_loop/test.desc

Line 3 in 61fd24d

--apply-loop-contracts _ --unsigned-overflow-check

[feliperodri]

I moved the flag to specific test cases. However, which behaviors would we want to test on invalid pointers? If CPROVER API says we can't use these primitives with invalid pointers, we should only use function contracts with --pointer-primitive-check, right?

[SaswatPadhi]

We may not specifically be checking any behavior for invalid pointers (although we might want to, in some form, in the future, see: #6238), but within the "contracts" regression suite, we shouldn't necessarily have to always create allocated pointers. Some property checks work just fine with uninitialized pointers and that might be sufficient for some cases.

One last question I have is regarding the need for this check. The memory primitives documentation (http://cprover.diffblue.com/memory-primitives.html) says that the check is necessary only for memory primitives. We don't seem to use them in the test cases directly. Do we generate them during instrumentation?

[feliperodri]

Do we generate them during instrumentation?

Yes, we do. We rely on them to check frame conditions. We use __CPROVER_same_object, __CPROVER_POINTER_OFFSET, and __CPROVER_OBJECT_SIZE. For instance, take a look at this

cbmc/src/goto-instrument/contracts/assigns.cpp

Lines 68 to 69 in b60259a

	// __CPROVER_same_object(lhs, target)
	condition.push_back(same_object(lhs_ptr, target));

[feliperodri]

Other than that, can we add a test case where we assign to a local variable with the same name as the global variable and make sure that things work correctly?

Done! Could you take another look? @SaswatPadhi

[SaswatPadhi]

Thanks for adding the new test case.

LGTM modulo a minor comment below.