label_properties: do not rely on source_locationt's get_function() #4131

tautschnig · 2019-02-08T11:06:16Z

A source location is a place in a text file, and the function information stored
in there need not coincide with the name we use in the goto model.

Part 1: label_properties should use the actual function name so that properties
in different instantiations of a function (as may happen when linking static
functions) get unique names.

This is in parts an RFC: it may actually be the right thing to use source_locationt::get_function for this purpose and no change should be made.

Each commit message has a non-empty body, explaining why the change was made.
n/a 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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

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

kroening · 2019-02-12T11:54:18Z

I think that there are two cases to consider:

Preconditions: these should get an ID that matches the caller, not the callee
Inlining. I would say that the ID should match the callee.

A problem with source_location.get_function() could be decoration to resolve overloading. Do we want an ID like some_class.whatnot(int, blub).property1? Or do we want something shorter?

kroening · 2019-02-12T11:55:57Z

Another issue is file-local functions. Say multiple instances of some static function. They all have the same get_function(), and then some other layer of disambiguation needs to happen.

peterschrammel · 2019-03-06T21:13:06Z

I'm pretty much open to what the property IDs look like. It's convenient if they are somehow related to the function that contains the assertion, but I wouldn't complain if they were just a sequence number or a hash in order to limit their length.

TGWDB · 2021-09-15T09:11:03Z

Closing this as having unresolved status on whether it is the right thing to do as well as being untouched for a couple of years. Please reopen if you believe this is erroneous and can update with a path towards a correct answer.

kroening · 2022-10-13T10:34:42Z

Reopening since we still very much want something like this.

tautschnig · 2022-10-13T11:10:43Z

Rebased, but various regression test failures need to be debugged.

feliperodri · 2022-11-28T19:07:57Z

regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --dfcc main --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
-^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$


For contracts, we should not refer to the wrapper function, but to the original function (i.e., foo). The user should identify the assignment in the original function that violates the assigns clause. We might want to keep the change from this PR, but fix this in our instrumentation. (cc. @remi-delmas-3000 )

Yes let's keep it like this in this PR, I'll fix generated locations in contracts in a different PR

One way to fix this (but I might be missing something) is to rename the original function instead?!

remi-delmas-3000 · 2022-12-06T16:39:00Z

I don't understand how deprecating get/set_function solves the problems we currently have ?

Is it by forcing us developers in each different context to think harder about where to get a meaningful function ID from ? (instead of reaching for the method that sounds like it gives us what we want).

How about adding a section in the developer manual with high level guidance on properties/locations things should be presented to the user, at least in cases mentioned above (preconditions/postconditions, in the presence of inlining, in the presence of name mangling, when inserting generic checks, etc.).

tautschnig · 2022-12-06T17:34:13Z

I don't understand how deprecating get/set_function solves the problems we currently have ?

Is it by forcing us developers in each different context to think harder about where to get a meaningful function ID from ? (instead of reaching for the method that sounds like it gives us what we want).

Yes. That current function produces an arbitrary string that might be good enough for presenting information to a (human) user, but even then could be confusing (think: inlining). Using it to solve other problems in the code base will almost always be wrong, and when it's (seemingly) the only option we have then we might have to build new means for solving the problem.

How about adding a section in the developer manual with high level guidance on properties/locations things should be presented to the user, at least in cases mentioned above (preconditions/postconditions, in the presence of inlining, in the presence of name mangling, when inserting generic checks, etc.).

If we end up retaining get_function(), then we will inevitably need to add guidance to the manual on when (not) to use it. Is that the kind of documentation you are suggesting we add?

remi-delmas-3000

When checking a function contract on function foo, we rename foo to foo_wrapped_for_contract_checking or __CPROVER_contracts_original_foo in the GOTO functions map but source locations for all instructions keep the foo function attribute.

The original foo function becomes the verification wrapper which is good because pre/post conditions are labelled with foo.

We wanted the mangling to remain transparent to the user and wanted the original funciton id to be used in both wrapper function and original function assertions, but with this change the mangled function name gets exposed in the property id.
Right now apart from doing a specific pass to fix the property_ids afterwards I don't see how to achieve the desired output.

remi-delmas-3000 · 2022-12-06T16:20:42Z

regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --dfcc main --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
-^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$


Yes let's keep it like this in this PR, I'll fix generated locations in contracts in a different PR

remi-delmas-3000 · 2022-12-06T16:25:03Z

src/goto-programs/show_properties.h

@@ -45,11 +45,10 @@ void show_properties(
 /// \param property: irep_idt that identifies property


is this the property class (e.g. assert, assigns, precondition, etc.) ?

No, this is the full property identifier (a unique key).

remi-delmas-3000 · 2023-01-12T17:40:51Z

src/goto-programs/show_properties.h

@@ -45,11 +45,10 @@ void show_properties(
 /// \param property: irep_idt that identifies property
 /// \param goto_functions: program in which to search for
 ///   the property
-/// \return optional<source_locationt> the location of the
+/// \return A pair of function identifier and source location of the


Suggestion: "A pair of function identifier and source location, where the function identifier is that of the GOTO function that contains the ASSERT instructions matching the property, and the source location is that of the ASSERT instruction matching the property. The function identifier and source location's function attribute are not necessarily equal."

Thank you, I've updated this comment.

peterschrammel

Maybe we should distinguish between GOTO function and "source function"? What you would like to see in the property names is the source function whereas get_function returns the GOTO function (and is required to return the GOTO function in some places in the code). Source function would then always track the original C function a goto statement is associated with/has been derived from.

tautschnig · 2023-02-04T21:20:57Z

Maybe we should distinguish between GOTO function and "source function"? What you would like to see in the property names is the source function whereas get_function returns the GOTO function (and is required to return the GOTO function in some places in the code). Source function would then always track the original C function a goto statement is associated with/has been derived from.

Well, but that "source function" is not necessarily unique (just consider static (file-local) functions). So it can't trivially be used as the prefix of property identifiers.

A source location is a place in a text file, and the function information stored in there need not coincide with the name we use in the goto model. In this vein, label_properties should use the actual function name so that properties in different instantiations of a function (as may happen when linking static functions) get unique names.

tautschnig added the RFC Request for comment label Feb 8, 2019

tautschnig assigned kroening and peterschrammel Feb 8, 2019

tautschnig requested review from cesaro, chrisr-diffblue, cristina-david, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli and smowton as code owners February 8, 2019 11:06

allredj reviewed Feb 8, 2019

View reviewed changes

TGWDB closed this Sep 15, 2021

tautschnig mentioned this pull request Oct 13, 2022

deprecate source_locationt::get/set_function #7239

Merged

2 tasks

kroening reopened this Oct 13, 2022

tautschnig self-assigned this Oct 13, 2022

tautschnig changed the title ~~[RFC] label_properties: Only use source_locationt's get_function() for user output~~ label_properties: do not rely on source_locationt's get_function() Oct 13, 2022

tautschnig force-pushed the properties-get_function branch from 2ff8e7a to 25bd89d Compare October 13, 2022 11:10

tautschnig requested review from romainbrenguier and chris-ryder as code owners October 13, 2022 11:10

tautschnig marked this pull request as draft October 13, 2022 11:10

tautschnig removed the request for review from cesaro October 14, 2022 08:29

tautschnig removed the RFC Request for comment label Nov 9, 2022

tautschnig force-pushed the properties-get_function branch from bdf278b to d774afe Compare November 20, 2022 21:44

tautschnig self-assigned this Nov 21, 2022

tautschnig force-pushed the properties-get_function branch from d774afe to cb8c5f3 Compare November 21, 2022 12:49

tautschnig removed their assignment Nov 21, 2022

feliperodri added the aws-medium label Nov 21, 2022

feliperodri reviewed Nov 28, 2022

View reviewed changes

feliperodri removed their assignment Nov 28, 2022

feliperodri added the Needs rebase label Jan 9, 2023

tautschnig removed the Needs rebase label Jan 11, 2023

tautschnig force-pushed the properties-get_function branch 2 times, most recently from 7b50599 to 1a0fe1b Compare January 11, 2023 12:47

remi-delmas-3000 reviewed Jan 12, 2023

View reviewed changes

peterschrammel reviewed Jan 16, 2023

View reviewed changes

tautschnig self-assigned this Jan 30, 2023

feliperodri removed aws Bugs or features of importance to AWS CBMC users aws-medium labels Jan 30, 2023

tautschnig force-pushed the properties-get_function branch from 1a0fe1b to fc24af0 Compare February 4, 2023 21:25

tautschnig removed their assignment Feb 4, 2023

tautschnig force-pushed the properties-get_function branch from fc24af0 to 3e8d1d5 Compare February 23, 2023 10:05

tautschnig self-assigned this May 31, 2023

tautschnig added the Needs rebase label May 31, 2023

tautschnig force-pushed the properties-get_function branch from 3e8d1d5 to 4dc81d5 Compare June 1, 2023 18:59

tautschnig removed the Needs rebase label Jun 1, 2023

tautschnig mentioned this pull request Nov 7, 2023

List of cleanup locations marked as DEPRECATED #7998

Open

23 tasks

NlightNFotis mentioned this pull request Nov 13, 2023

src/util/source_location.h - set_function and get_function #8026

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

label_properties: do not rely on source_locationt's get_function() #4131

label_properties: do not rely on source_locationt's get_function() #4131

tautschnig commented Feb 8, 2019

allredj left a comment

kroening commented Feb 12, 2019

kroening commented Feb 12, 2019 •

edited

Loading

peterschrammel commented Mar 6, 2019

TGWDB commented Sep 15, 2021

kroening commented Oct 13, 2022

tautschnig commented Oct 13, 2022

feliperodri Nov 28, 2022

remi-delmas-3000 Dec 6, 2022

tautschnig Dec 6, 2022

remi-delmas-3000 commented Dec 6, 2022

tautschnig commented Dec 6, 2022

remi-delmas-3000 left a comment

remi-delmas-3000 Dec 6, 2022

remi-delmas-3000 Dec 6, 2022

tautschnig Feb 4, 2023

remi-delmas-3000 Jan 12, 2023

tautschnig Feb 4, 2023

peterschrammel left a comment •

edited

Loading

tautschnig commented Feb 4, 2023

		@@ -45,11 +45,10 @@ void show_properties(
		/// \param property: irep_idt that identifies property

label_properties: do not rely on source_locationt's get_function() #4131

Are you sure you want to change the base?

label_properties: do not rely on source_locationt's get_function() #4131

Conversation

tautschnig commented Feb 8, 2019

allredj left a comment

Choose a reason for hiding this comment

kroening commented Feb 12, 2019

kroening commented Feb 12, 2019 • edited Loading

peterschrammel commented Mar 6, 2019

TGWDB commented Sep 15, 2021

kroening commented Oct 13, 2022

tautschnig commented Oct 13, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

remi-delmas-3000 commented Dec 6, 2022

tautschnig commented Dec 6, 2022

remi-delmas-3000 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

peterschrammel left a comment • edited Loading

Choose a reason for hiding this comment

tautschnig commented Feb 4, 2023

kroening commented Feb 12, 2019 •

edited

Loading

peterschrammel left a comment •

edited

Loading