A few permutations for stack-list.c0 benchmark failed with the following error:
Error with Perm ID= 11242: c0rt: /tmp/temp_src1568849558655235016.c0: 178.5-178.23: assert failed88
The reason was a mis-translated run-time check in the push function.
The assignment below
n->next = s->top;
...
s->top = n;
Causes the symbolic value for s->top to get updated in the state with n's value, which is fine except for the fact that the old symbolic value for s->top, which is stored at n->next, looks like s@3@04.Stack$top@26@04. So, when the translator tries to reverse the s@3@04.Stack$top@26@04.Node$next@35@04 after s->top = n there are issues. The translator should produce s->top->next->next or n->next->next, but it incorrectly returns s->top->next.
Since s@3@04.Stack$top@26@04.Node$next@35@04 is fresh from optimistic framing, it will have to be regex translated, which is fine. .next is pulled out and s@3@04.Stack$top@26@04 is translated. This is where the issue comes in. Currently, the translator is strictly translating s@3@04.Stack$top@26@04, which means it looks for the direct objects of it in the store and heaps. Since this value comes from the regex function, it won't be found initially in the store or heaps (even though n->next is mapped to it in the heap). As a result, s@3@04.Stack$top@26@04 is regex translated again and again ultimately resulting in s->top->next. The translator does look for and translates heap aliases later, so it does produce n->next->next correctly as well. But, s->top->next is chosen by the translator since it was produced first.
A simple solution to this problem is to allow lenient look-up for s@3@04.Stack$top@26@04 out of the regex call. This way regex is officially the last resort for translation. This should hopefully keep bad results like s->top->next being produced at all.
jennalwise
commented
1 year ago
A few permutations for
stack-list.c0benchmark failed with the following error:The reason was a mis-translated run-time check in the
pushfunction.The assignment below
Causes the symbolic value for
s->topto get updated in the state withn's value, which is fine except for the fact that the old symbolic value fors->top, which is stored atn->next, looks likes@3@04.Stack$top@26@04. So, when the translator tries to reverse thes@3@04.Stack$top@26@04.Node$next@35@04afters->top = nthere are issues. The translator should produces->top->next->nextorn->next->next, but it incorrectly returnss->top->next.Since
s@3@04.Stack$top@26@04.Node$next@35@04is fresh from optimistic framing, it will have to be regex translated, which is fine..nextis pulled out ands@3@04.Stack$top@26@04is translated. This is where the issue comes in. Currently, the translator is strictly translatings@3@04.Stack$top@26@04, which means it looks for the direct objects of it in the store and heaps. Since this value comes from the regex function, it won't be found initially in the store or heaps (even though n->next is mapped to it in the heap). As a result,s@3@04.Stack$top@26@04is regex translated again and again ultimately resulting ins->top->next. The translator does look for and translates heap aliases later, so it does producen->next->nextcorrectly as well. But,s->top->nextis chosen by the translator since it was produced first.A simple solution to this problem is to allow lenient look-up for
s@3@04.Stack$top@26@04out of the regex call. This way regex is officially the last resort for translation. This should hopefully keep bad results likes->top->nextbeing produced at all.