Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

FS-25 Try 2 #13

Merged
merged 5 commits into from
Feb 1, 2021
Merged

FS-25 Try 2 #13

merged 5 commits into from
Feb 1, 2021

Conversation

cd1m0
Copy link
Collaborator

@cd1m0 cd1m0 commented Jan 29, 2021

This PR is based on work done by @norhh here #11. The previous PR did a lot of good work to uncover all of the places we need to fix to handle shadowing. However, the fixes in that PR were complicated by the fact that a lot of the code they touched was not well written (by me) and over-complicated. This got in the way of fixing.

In this PR we attempt to first fix the problems in the code, and then to add code to handle the various cases of name collisions/shadowing. In detail:

  1. Cleanup:
    • Convert the InstrumentationContext interface into its own utility class. The InstrumentationContext class is responsible for keeping toghether all state shared between the instrumentation of all invariants

    • Rename UIDGenerator to the better NameGenerator and move it inside of InstrumentationContext (it used to be a global var)

    • Add the existingNames field to NameGenerator to allow it to avoid all names that existed in the original AST

    • Convert several constants from global constant strings into fields of InstrumentationContext. Furthermore the values of these fields were obtained by calling into NameGenerator. This guarantees that they wont overlap with existing names, and all future instrumentation names wont conflict with them. This includes:

      SCRIBBLE_VAR -> InstrumentationContext.structVar
      REENTRANCY_UTILS_CONTRACT -> InstrumentationContext.utilsContractName
      CHECK_STATE_INVS_FUN -> InstrumentationContext.checkStateInvsFuncName
      OUT_OF_CONTRACT -> InstrumentationContext.outOfContractFlagName

    • Introduced the InstrumentationContext.internalInvariantCheckers map and corresponding function getInternalInvariantCheckerName(ContractDefinition) to generate names for the internal contract-invariant checker helper function without collisions.

    • Changed the code in interpose(..) to use NameGenerator when renaming the original functions to avoid collisions

    • Added the TranspilingContext class. It contains the state that is need to compile JUST the annotations for one function/contract. This includes a reference to InstrumentationContext, as well as the typing and semantic information for the group of annotations for the given function/contract.

    • Changed flattenExpr and generateExpressions to take a TranspilingContext instead of the jumble of arguments they had before

    • Changed the flattening and AST generation code to use TranspilingContext when computing field names for let-bindings, internal let-vars, internal old-vars as well as some other internals such as the scratch field (what used to be MSTORE_SCRATCH_FIELD) and the CHECK_INVS_AT_END flag.

    • Added tests (see test/samples/increment_inherited_collision.sol).

cd1m0 added 5 commits January 27, 2021 20:23
…strumentationContext; Add set of all known names from all source units to NameGenerator, and capability to avoid collisions
…ility contract (in generateUtilsContract). Convert the __scribble_check_state_invariants, __scribble_out_of_contract and __scribble_ReentrancyUtils constants into nameGenerator accesses.
…ctionInstrumenter.insertEnterMarker, FunctionInstrumetner.insertExitMarker to use TranspilingContext; Convert naming of temp bindings struct fields to use TranspilingContext to avoid collisions;
@cd1m0 cd1m0 requested review from blitz-1306 and norhh January 29, 2021 08:11
Copy link
Contributor

@blitz-1306 blitz-1306 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good. Just a smaller suggestion.

@@ -0,0 +1,39 @@
export class NameGenerator {
private counters: { [base: string]: number };
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can use the object here, ofcourse. But would be cool to have a Map<string, number> instead. It may have some builerplate code, but on large amount of keys it would be more efficient.

Copy link
Contributor

@norhh norhh left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good

@cd1m0 cd1m0 merged commit e27db5e into develop Feb 1, 2021
@cd1m0 cd1m0 mentioned this pull request Feb 1, 2021
@blitz-1306 blitz-1306 deleted the fs25-dimo branch February 2, 2021 03:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants