CONTRACTS: filter out contract symbols when resolving entry points and interrupt handlers

[remi-delmas-3000]

Contract symbols (#6799) have the same base name as the function symbol they are derived from.
This causes both the function and its contract to be found when doing a lookup by base name,
when resolving entry points for instance.

We now filter out symbols that have the is_property set when resolving entry points and interrupt handlers.

• 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.
• [N/A] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• [N/A] 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).
• [N/A] 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.

[tautschnig]

Where exactly are we assuming the base name to be unambiguous? I don’t think this should be done anywhere: imagine a local variable named “main”, which is perfectly legitimate.

[codecov]

Codecov Report

Merging #7063 (1c79f1f) into develop (d7b3f48) will increase coverage by 0.00%.
The diff coverage is 75.00%.

❗ Current head 1c79f1f differs from pull request most recent head 50dd44b. Consider uploading reports for the commit 50dd44b to get more accurate results

@@            Coverage Diff            @@
##           develop    #7063    +/-   ##
=========================================
  Coverage    77.86%   77.86%            
=========================================
  Files         1569     1576     +7     
  Lines       180995   181808   +813     
=========================================
+ Hits        140929   141573   +644     
- Misses       40066    40235   +169     

Impacted Files	Coverage Δ
src/goto-instrument/interrupt.cpp	0.00% <ø> (ø)
src/jsil/jsil_entry_point.cpp	0.00% <0.00%> (ø)
src/ansi-c/ansi_c_entry_point.cpp	89.45% <100.00%> (ø)
src/ansi-c/c_typecheck_base.cpp	82.50% <100.00%> (ø)
src/cpp/cpp_template_type.h	52.94% <0.00%> (-11.35%)	⬇️
src/util/pointer_expr.h	80.83% <0.00%> (-7.29%)	⬇️
src/goto-programs/goto_convert.cpp	88.12% <0.00%> (-4.22%)	⬇️
src/solvers/flattening/boolbv_quantifier.cpp	89.91% <0.00%> (-3.37%)	⬇️
src/ansi-c/c_typecheck_expr.cpp	74.17% <0.00%> (-3.09%)	⬇️
src/pointer-analysis/value_set_fi.h	90.76% <0.00%> (-3.08%)	⬇️
... and 87 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

[remi-delmas-3000]

The ambiguity surfaced here where entry points are looked up by base_name :

cbmc/src/ansi-c/ansi_c_entry_point.cpp

Line 145 in 78efc2c

if(matches.size()>=2)

The lookup finds both the function symbol and the contract symbol and bails out. In particular, this means that we cannot use a function that has a contract as an entry point for contract checking like we used to do before.

What would be the problem with making it a truly unique symbol (i.e. name, base_name and pretty_name all unique) ?

[martin-cs]

Seems legit but note @tautschnig 's concern.

[tautschnig]

The ambiguity surfaced here where entry points are looked up by base_name :

cbmc/src/ansi-c/ansi_c_entry_point.cpp

Line 145 in 78efc2c

if(matches.size()>=2)

We should fix

cbmc/src/ansi-c/ansi_c_entry_point.cpp

Line 133 in 78efc2c

if(s_it->second.type.id()==ID_code)

to filter out ones that have symbol.is_property set.

The lookup finds both the function symbol and the contract symbol and bails out. In particular, this means that we cannot use a function that has a contract as an entry point for contract checking like we used to do before.

Yes, indeed this needs to be fixed, but I think it should be done as suggested above.

What would be the problem with making it a truly unique symbol (i.e. name, base_name and pretty_name all unique) ?

I don't think that that would be a problem, I just don't think it's the right fix for what actually is a problem.

[remi-delmas-3000]

Hi again, before implementing your suggestion, please hear me out once again :)

I found at least 8 other places where symbol_base_map is used for lookups and for each of these places we have to figure out if the duplicate match would cause a problem or not.

Making the base name unique would make the impact of adding contract:: symbols more local and transparent to the rest of the codebase.

[kroening]

It would be highly unusual to stick a prefix before a base_name.

[remi-delmas-3000]

@tautschnig @kroening, now filtering out contracts from lookups by base name