C entry point generator: no unconditional conversion to pointer type #6976

tautschnig · 2022-06-28T09:18:16Z

Do not try to create a pointer_typet when the type might not actually be
a pointer type. This was triggerable by syntactically well-formed C
input and should instead be handled by a user-facing error message.

Fixes: #6975

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.
n/a 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.

kroening · 2022-06-28T10:04:35Z

src/ansi-c/ansi_c_entry_point.cpp

@@ -248,7 +248,10 @@ bool generate_ansi_c_start_function(
    {
      // ok
    }
-    else if(parameters.size()==2 || parameters.size()==3)
+    else if(
+      parameters.size() >= 2 && parameters[1].type().id() == ID_pointer &&


Did you mean parameters[0]?

No, parameters[0] is what we'd expect to be argc if I' not mistaken?

This looks wrong because the regression test has (char *argv, int argc) but the CBMC code is expecting/assuming the parameters in the other order. Is there a place where the code rewrites/forces the order, or is this actually entirely up to the code being sent to CBMC? If the former, a comment would clarify this, if the latter, then this code makes assumptions that may be wrong.

The one place that enforces the order is the C standard (and any related architecture descriptions). The user, however, may supply arbitrary (syntactically valid) C code, even one that does not respect the calling conventions set out in the C standard. If the user does supply such code (as is done in the accompanying regression test), then we can only tell them that they got it wrong, which is what we do via the error message in the else branch of this code. The change being proposed here should make sure that we do end up in this else branch.

Does this address your concern? Should I still be making changes to the implementation? Should I perhaps add the above as a comment?

Yes, I'm happy to approve. The detail in your response might be nice to have in the comments though since this is not immediately clear.

Comment added to the code.

The comment is very helpful.

codecov · 2022-06-28T10:25:32Z

Codecov Report

Base: 77.88% // Head: 77.88% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (6f96674) compared to base (c764c1d).
Patch coverage: 100.00% of modified lines in pull request are covered.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #6976   +/-   ##
========================================
  Coverage    77.88%   77.88%           
========================================
  Files         1576     1576           
  Lines       181856   181859    +3     
========================================
+ Hits        141645   141648    +3     
  Misses       40211    40211

Impacted Files	Coverage Δ
src/util/expr.h	`97.02% <ø> (ø)`
src/ansi-c/ansi_c_entry_point.cpp	`89.57% <100.00%> (+0.12%)`	⬆️

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

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

TGWDB · 2022-08-17T09:14:54Z

src/ansi-c/ansi_c_entry_point.cpp

@@ -248,7 +248,10 @@ bool generate_ansi_c_start_function(
    {
      // ok
    }
-    else if(parameters.size()==2 || parameters.size()==3)
+    else if(
+      parameters.size() >= 2 && parameters[1].type().id() == ID_pointer &&


Yes, I'm happy to approve. The detail in your response might be nice to have in the comments though since this is not immediately clear.

nwetzler

This looks like a great solution. Only suggestion would be to add more detail to the regression test about what the test is aiming to achieve.

nwetzler · 2022-09-27T23:18:50Z

src/ansi-c/ansi_c_entry_point.cpp

@@ -248,7 +248,10 @@ bool generate_ansi_c_start_function(
    {
      // ok
    }
-    else if(parameters.size()==2 || parameters.size()==3)
+    else if(
+      parameters.size() >= 2 && parameters[1].type().id() == ID_pointer &&


The comment is very helpful.

nwetzler · 2022-09-27T23:21:40Z

regression/ansi-c/main1/test.desc

+^EXIT=(64|1)$
+^SIGNAL=0$
+--
+Invariant check failed


Can we add a description of what the test is trying to achieve? Maybe something like:

In this test, we detect a non-standard C entry point and gracefully exit with a message to the user.

Thank you, done!

Do not try to create a pointer_typet when the type might not actually be a pointer type. This was triggerable by syntactically well-formed C input and should instead be handled by a user-facing error message. Fixes: diffblue#6975

tautschnig added bugfix C Front End labels Jun 28, 2022

tautschnig requested review from kroening and chris-ryder as code owners June 28, 2022 09:18

tautschnig assigned kroening and chris-ryder Jun 28, 2022

kroening reviewed Jun 28, 2022

View reviewed changes

tautschnig assigned TGWDB Jul 1, 2022

tautschnig force-pushed the bugfixes/6975-main-tc branch from 52307ed to b752c2d Compare August 12, 2022 07:53

TGWDB approved these changes Aug 17, 2022

View reviewed changes

tautschnig assigned tautschnig and unassigned TGWDB Aug 17, 2022

tautschnig force-pushed the bugfixes/6975-main-tc branch from b752c2d to e86af02 Compare September 22, 2022 14:31

tautschnig removed their assignment Sep 22, 2022

jimgrundy requested a review from nwetzler September 25, 2022 21:14

nwetzler approved these changes Sep 27, 2022

View reviewed changes

tautschnig force-pushed the bugfixes/6975-main-tc branch from e86af02 to 6f96674 Compare September 28, 2022 07:47

kroening approved these changes Sep 28, 2022

View reviewed changes

kroening merged commit 430acdd into diffblue:develop Sep 28, 2022

tautschnig deleted the bugfixes/6975-main-tc branch September 29, 2022 09:29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

C entry point generator: no unconditional conversion to pointer type #6976

C entry point generator: no unconditional conversion to pointer type #6976

Uh oh!

tautschnig commented Jun 28, 2022

Uh oh!

kroening Jun 28, 2022

Uh oh!

tautschnig Jun 28, 2022

Uh oh!

TGWDB Jul 1, 2022

Uh oh!

tautschnig Jul 1, 2022

Uh oh!

TGWDB Aug 17, 2022

Uh oh!

tautschnig Sep 22, 2022

Uh oh!

nwetzler Sep 27, 2022

Uh oh!

codecov bot commented Jun 28, 2022 •

edited

Loading

Uh oh!

TGWDB Aug 17, 2022

Uh oh!

nwetzler left a comment

Uh oh!

nwetzler Sep 27, 2022

Uh oh!

nwetzler Sep 27, 2022

Uh oh!

tautschnig Sep 28, 2022

Uh oh!

Uh oh!

C entry point generator: no unconditional conversion to pointer type #6976

C entry point generator: no unconditional conversion to pointer type #6976

Uh oh!

Conversation

tautschnig commented Jun 28, 2022

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Jun 28, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nwetzler left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Jun 28, 2022 •

edited

Loading