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

Fix and refactor decoder and translator #28

Merged
merged 4 commits into from
Jun 29, 2023

Conversation

sergeypospelov
Copy link
Member

@sergeypospelov sergeypospelov commented Jun 28, 2023

This PR fixes the problem with UModelBase ambiguity and refactors the whole decoding mechanism a little bit.

Details

The problem

We analyze function check:

int check(A a0) {
    int x = a0.x; // here we first check for NPE and get a case with an exception
    if (x == 0) {
        return 0;
    }
    return 1;
}
  1. Suppose we do fast-check a0 == 0 in empty UModel and it has empty m0: KModel, so a0 evaluates to sample value null, because register reading was not translated yet.
  2. Then we translate register reading into r0 := mkConst("r0") and for some reason m0(r0) equals to something different from null.
  3. Then we resolve the exceptional case into JcTest and read r0 from the model m0, but now the model contains r0, we get something non-null, and that is the problem.

To fix that, we provide an expression translator in every component of UModelBase, so it first translates an expression and only then the expression is evaluated in a KModel.

Other

I decided to remove UCachingExprTranslator to simplify extension of our expressions and the total number of components. Now, UExprTranslator caches UExprs via KNonRecursiveTransformer and also caches initial values for URegionIds explicitly.

Lazy model components calls translate function, which takes an expression from a cache or explicitly transforms it.

Also fixed cache usage in UTreeMemoryUpdatesFolder visitor a little bit.

@sergeypospelov sergeypospelov merged commit 41f1db6 into main Jun 29, 2023
@sergeypospelov sergeypospelov mentioned this pull request Jul 3, 2023
24 tasks
korifey pushed a commit that referenced this pull request Jul 12, 2023
@sergeypospelov sergeypospelov deleted the sergey/umodel_translator_fix branch July 17, 2023 06:47
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.

2 participants