Quite a few list.c0 benchmark files for one random increment is resulting in this error Non-variable argument given to Store.getKeyForValue: (Second: (Second: $t@15@01)). This is due to symbolic values of the type that relates to (Second: (Second: $t@15@01)) not being supported by Store.getKeyForValue.
Store.getKeyForValue should not be called with non-variable types.
One reason Store.getKeyForValue is being called with non-variable types is because the regularVariableResolver is not receiving the correct heaps for translation when predicate bodies or method postconditions are being produced at unfold statements and method call statements respectively. Local variables to predicate bodies and method contracts can be assigned with symbolic values from the heap or optimistic heap that exist before the unfold or the method call. So those same variables that are being produced in the predicate body or method postcondition are creating symbolic values that can only be translated with the old heaps (including the optimistic heap). However, fields in the predicate body or post condition need to be translated with the current state since their values may be different or fresh from before the unfold or method call. Therefore, we need to translate with heaps that contain both the before heap chunks and the current heap chunks. This problem/solution is an edge case of the solution for variable mismatch for folds/unfolds and method calls to solve this issue https://github.com/gradual-verification/silicon-gv/issues/25, and just like we are tracking old stores we need to track old heaps and old optimistic heaps for translation.
Solution Outline/Notes:Consumes in folds/unfolds/method calls do not need the old heaps for variables and heap locations because they always reference the old heaps anyway. Produce evaluates heap locations using the current heaps, so to translate them back to the original expression we need the current heaps. Local variables for predicate bodies or method calls are evaluated to symbolic values in the store that were created from heap values from a pre/old state. So, translation needs to occur with heaps that contain all the values, both current and old heap values. Whenever the old store is set, then also set up the proper heaps for translation as the old store being set indicates we are at a fold/unfold/method call that needs to also have translation with an old state.
After fixing the above old/current heap issue, Store.getKeyForValue is still being called in List.vpr’s full static solution with a non-variable symbolic value. It looks like the problem is that the translator is not finding the correct symbolic value in the heap when it is there for the loop condition in list.vpr. In particular, it cannot find curr.Node$next in curr.Node$next.Node$val < val . Problem is that the symbolic value for curr.Node$next.Node$val is being found in the the heap at (First: (Second: $t@23@01)).Node$next. So, (First: (Second: $t@23@01)) is being returned to regularVariableResolver and that is being looked up in store.getKeyForValue(..). Instead, I think we should probably just call variableResolver on the result instead of store.getKeyForValue(..), because (First: (Second: $t@23@01)) also needs to be looked up in the heap. This is probably true for the optimisticHeap lookup case in regularVariableResolver as well. Also, similarly modified in Translator.getAccessibilityPredicates.
jennalwise
commented
2 years ago
Quite a few
list.c0benchmark files for one random increment is resulting in this errorNon-variable argument given to Store.getKeyForValue: (Second: (Second: $t@15@01)). This is due to symbolic values of the type that relates to(Second: (Second: $t@15@01))not being supported byStore.getKeyForValue.Store.getKeyForValueshould not be called with non-variable types.One reason
Store.getKeyForValueis being called with non-variable types is because theregularVariableResolveris not receiving the correct heaps for translation when predicate bodies or method postconditions are being produced at unfold statements and method call statements respectively. Local variables to predicate bodies and method contracts can be assigned with symbolic values from the heap or optimistic heap that exist before the unfold or the method call. So those same variables that are being produced in the predicate body or method postcondition are creating symbolic values that can only be translated with the old heaps (including the optimistic heap). However, fields in the predicate body or post condition need to be translated with the current state since their values may be different or fresh from before the unfold or method call. Therefore, we need to translate with heaps that contain both the before heap chunks and the current heap chunks. This problem/solution is an edge case of the solution for variable mismatch for folds/unfolds and method calls to solve this issue https://github.com/gradual-verification/silicon-gv/issues/25, and just like we are tracking old stores we need to track old heaps and old optimistic heaps for translation.Solution Outline/Notes:
Consumesin folds/unfolds/method calls do not need the old heaps for variables and heap locations because they always reference the old heaps anyway.Produceevaluates heap locations using the current heaps, so to translate them back to the original expression we need the current heaps. Local variables for predicate bodies or method calls are evaluated to symbolic values in the store that were created from heap values from a pre/old state. So, translation needs to occur with heaps that contain all the values, both current and old heap values. Whenever the old store is set, then also set up the proper heaps for translation as the old store being set indicates we are at a fold/unfold/method call that needs to also have translation with an old state.After fixing the above old/current heap issue,
Store.getKeyForValueis still being called inList.vpr’s full static solution with a non-variable symbolic value. It looks like the problem is that the translator is not finding the correct symbolic value in the heap when it is there for the loop condition inlist.vpr. In particular, it cannot findcurr.Node$nextincurr.Node$next.Node$val < val. Problem is that the symbolic value forcurr.Node$next.Node$valis being found in the the heap at(First: (Second: $t@23@01)).Node$next. So,(First: (Second: $t@23@01))is being returned toregularVariableResolverand that is being looked up instore.getKeyForValue(..). Instead, I think we should probably just callvariableResolveron the result instead ofstore.getKeyForValue(..), because(First: (Second: $t@23@01))also needs to be looked up in the heap. This is probably true for the optimisticHeap lookup case inregularVariableResolveras well. Also, similarly modified inTranslator.getAccessibilityPredicates.