gradual-verification / silicon-gv

Mozilla Public License 2.0
0 stars 3 forks source link

Regex Handler in Translator needs to handle cases like (Second: $t@10@01).Node$total@20@01 #32

Closed jennalwise closed 2 years ago

jennalwise commented 2 years ago

Composite.c0 benchmark is creating files that are having trouble translating (Second: $t@10@01).Node$total@20@01 in (== node@2@01.Node$total@19@01 (+ (+ 1 node@2@01.Node$left@11@01.Node$total@12@01) (Second: $t@10@01).Node$total@20@01)) for a run-time check created by consuming the body of context(left, node, left->total) from the fold (//@fold context(left, node, left->total);) in tree_get_left on line 237. (Second: $t@10@01).Node$total@20@01 is a symbolic value that needs to be translated using the regex handler in the Translator, because no heap chunks exist for it in the heap or optimistic heap. However, when it was created its receiver did have a heap chunk for it in the heap, so the receiver ends up as (Second: $t@10@01). Right now the regex handler cannot deal with (Second: $t@10@01) as a receiver, but this edge case requires it to. We probably should expect any receiver of a regex handler argument to possibly look like this and handle it accordingly.

jennalwise commented 2 years ago

Fixed here: https://github.com/gradual-verification/silicon-gv/commit/3c948e15eafcba3c8204d1931914a0c59dda9968