Symbol table transformer #321

vecchiot-aws · 2021-07-09T19:18:10Z

Description of changes:

Introduces a visitor pattern for transforming the symbol table. An example identity transformation is included to show the setup, and any of the default methods can be overridden to change behavior. Adds a compiler flag to list out symbol table passes to perform after codegenning.

Resolved issues:

Resolves #291

Call-outs:

Todo:

Documentation

Testing:

How is this change tested? Existing regression suite, plus new unit test suite specific to the symbol table transformer trait.
Is this a refactor change? No.

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

avanhatt

High level thoughts:

Visitor pattern implementation seems clean, straightforward, and useful.
Before landing, I would want to see some fairly heavy testing of this. Can we add a separate script that runs this over existing tests and checks that the identity is indeed correct? And that we can do simple changes, like inverting every boolean or similar?

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs

avanhatt · 2021-07-12T14:39:44Z

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs

Can we add a constructor that enforces this invariant?

Maybe I should make the comment more clear, but this means manually wrapped in .array_to_ptr() after construction (the other constructor does it for you).

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/transformer.rs

adpaco-aws

What about having the thing you are transforming be the second part of the function names?

For example, transform_type_... when transforming types, transform_expr_... when transforming expressions, and so on. Otherwise I feel like it's a bit harder to read/search, but maybe you've already considered this and decided this was the best way.

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/transformer.rs

vecchiot-aws · 2021-07-12T18:48:49Z

Before landing, I would want to see some fairly heavy testing of this. Can we add a separate script that runs this over existing tests and checks that the identity is indeed correct? And that we can do simple changes, like inverting every boolean or similar?

This has been manually checked, but I'm not sure what approach is best for automating it.

avanhatt · 2021-07-13T14:23:15Z

LGTM once some automated test is included in the PR (or, let me know if you feel like that should be a 2nd PR for timing).

avanhatt

LGTM!

danielsn

Might be nice to add something about this to a readme.

danielsn · 2021-07-20T14:07:13Z

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symtab_transformer/transformer.rs

+    }
+
+    /// Transform an assign expr (`left = right`)
+    /// Currently not able to be constructed, as does not exist in Rust


Constructor doesn't exist?

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

vecchiot-aws force-pushed the symbol-table-transformer branch from 4d5cfa5 to cd83ecd Compare July 9, 2021 20:35

vecchiot-aws marked this pull request as ready for review July 9, 2021 20:35

avanhatt suggested changes Jul 12, 2021

View reviewed changes

adpaco-aws reviewed Jul 12, 2021

View reviewed changes

vecchiot-aws force-pushed the symbol-table-transformer branch from cd83ecd to 65851cd Compare July 12, 2021 18:15

vecchiot-aws force-pushed the symbol-table-transformer branch 3 times, most recently from c5b36ca to 13192f3 Compare July 15, 2021 17:18

vecchiot-aws requested a review from avanhatt July 15, 2021 17:48

vecchiot-aws added 10 commits July 15, 2021 15:32

Create transformer trait.

a983e9a

Added identity transformer example.

96d3326

Rearranged; added compilation flag.

b666fcb

Added passes flag to rmc script.

f98954f

Add documentation.

9de3274

PR fixup.

0f28d47

Add unit tests for identity transformer.

b33ab24

Fix dry-run test.

535b873

Add to test script.

cf1b9b7

Fix compiler warnings.

d9ddad5

vecchiot-aws force-pushed the symbol-table-transformer branch from cba5f7d to d9ddad5 Compare July 15, 2021 19:33

vecchiot-aws changed the base branch from main-153-2021-07-09 to main-153-2021-07-15 July 15, 2021 19:34

avanhatt approved these changes Jul 16, 2021

View reviewed changes

Merge branch 'main-153-2021-07-15' into symbol-table-transformer

dda5b6e

vecchiot-aws mentioned this pull request Jul 19, 2021

Make --gen-c-runnable produce runnable C code #334

Merged

12 tasks

adpaco-aws approved these changes Jul 20, 2021

View reviewed changes

danielsn approved these changes Jul 20, 2021

View reviewed changes

danielsn merged commit 524b6f3 into model-checking:main-153-2021-07-15 Jul 20, 2021

adpaco-aws pushed a commit that referenced this pull request Jul 26, 2021

Symbol table transformer (#321)

053aafb

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

adpaco-aws pushed a commit that referenced this pull request Aug 2, 2021

Symbol table transformer (#321)

8fdd874

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

zhassan-aws mentioned this pull request Aug 6, 2021

fix bit logic operators #395

Closed

4 tasks

adpaco-aws pushed a commit that referenced this pull request Aug 6, 2021

Symbol table transformer (#321)

0553d29

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

adpaco-aws pushed a commit that referenced this pull request Aug 17, 2021

Symbol table transformer (#321)

674980a

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

adpaco-aws pushed a commit that referenced this pull request Aug 24, 2021

Symbol table transformer (#321)

05ea2a5

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Symbol table transformer (model-checking#321)

ccc6147

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

tedinski pushed a commit that referenced this pull request Apr 27, 2022

Symbol table transformer (#321)

cc60334

Adds a recursive visitor pattern which can be used to transform goto symbol tables, as well as a default (identity transform) implementation.

Symbol table transformer #321

Symbol table transformer #321

Uh oh!

Conversation

vecchiot-aws commented Jul 9, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Uh oh!

avanhatt left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

avanhatt Jul 12, 2021

Choose a reason for hiding this comment

Uh oh!

vecchiot-aws Jul 12, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

adpaco-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

vecchiot-aws commented Jul 12, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

avanhatt commented Jul 13, 2021

Uh oh!

avanhatt left a comment

Choose a reason for hiding this comment

Uh oh!

danielsn left a comment

Choose a reason for hiding this comment

Uh oh!

danielsn Jul 20, 2021

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

vecchiot-aws commented Jul 9, 2021 •

edited

Loading

vecchiot-aws commented Jul 12, 2021 •

edited

Loading