-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
479 do not backtranslate fancy sorts in get-model (#563)
Values of any sort other than `SortBool` and `SortInt` cannot currently be back-translated from the SMT representation (all sorts unknown to the solver are opaque). In particular, this is true for `Map`-sorted values (which are used frequently in EVM). * Do not attempt to back-translate values of sorts other than `SortBool` and `SortInt` * but still include the related SMT variables in the `get-values` requestl; * and indicate untranslated variables by adding `VAR = VAR` to the returned substitution. As shown in the added integration test, there are cases where the `Map`-sorted value is relevant, but cannot currently be returned. We might consider modeling `Map`s specifically as arrays in the SMT solver in the future. Fixes runtimeverification/kontrol#479
- Loading branch information
Showing
12 changed files
with
1,597 additions
and
573 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,5 +1,17 @@ | ||
| module TEST | ||
| imports INT | ||
| imports BOOL | ||
| imports MAP | ||
|
|
||
| // Int map definition from evm-semantics | ||
| syntax Int ::= #lookup ( Map, Int) [symbol(#lookup), function, total, smtlib(lookup)] | ||
| //------------------------------------------------------------------------------------- | ||
| rule [#lookup.some]: | ||
| #lookup( (KEY |-> VAL:Int) _M, KEY) => VAL | ||
| rule [#lookup.none]: | ||
| #lookup( M, KEY) => 0 requires notBool KEY in_keys(M) | ||
| rule [#lookup.notInt]: | ||
| #lookup( (KEY |-> VAL) _M, KEY) => VAL requires notBool isInt(VAL) | ||
| //------------------------------------------------------------------------------------- | ||
|
|
||
| endmodule |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
114 changes: 114 additions & 0 deletions
114
test/rpc-integration/test-get-model/response-with-map-relevant.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,114 @@ | ||
| { | ||
| "jsonrpc": "2.0", | ||
| "id": 1, | ||
| "result": { | ||
| "substitution": { | ||
| "format": "KORE", | ||
| "version": 1, | ||
| "term": { | ||
| "tag": "And", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortGeneratedTopCell", | ||
| "args": [] | ||
| }, | ||
| "patterns": [ | ||
| { | ||
| "tag": "Equals", | ||
| "argSort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| }, | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortGeneratedTopCell", | ||
| "args": [] | ||
| }, | ||
| "first": { | ||
| "tag": "EVar", | ||
| "name": "AMOUNT", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| } | ||
| }, | ||
| "second": { | ||
| "tag": "DV", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| }, | ||
| "value": "0" | ||
| } | ||
| }, | ||
| { | ||
| "tag": "Equals", | ||
| "argSort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| }, | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortGeneratedTopCell", | ||
| "args": [] | ||
| }, | ||
| "first": { | ||
| "tag": "EVar", | ||
| "name": "KEY", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| } | ||
| }, | ||
| "second": { | ||
| "tag": "DV", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| }, | ||
| "value": "0" | ||
| } | ||
| }, | ||
| { | ||
| "tag": "Equals", | ||
| "argSort": { | ||
| "tag": "SortApp", | ||
| "name": "SortMap", | ||
| "args": [] | ||
| }, | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortGeneratedTopCell", | ||
| "args": [] | ||
| }, | ||
| "first": { | ||
| "tag": "EVar", | ||
| "name": "Var'Ques'STORAGE", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortMap", | ||
| "args": [] | ||
| } | ||
| }, | ||
| "second": { | ||
| "tag": "EVar", | ||
| "name": "Var'Ques'STORAGE", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortMap", | ||
| "args": [] | ||
| } | ||
| } | ||
| } | ||
| ] | ||
| } | ||
| }, | ||
| "satisfiable": "Sat" | ||
| } | ||
| } |
7 changes: 7 additions & 0 deletions
7
test/rpc-integration/test-get-model/response-with-map-unsat.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,7 @@ | ||
| { | ||
| "jsonrpc": "2.0", | ||
| "id": 1, | ||
| "result": { | ||
| "satisfiable": "Unsat" | ||
| } | ||
| } |
7 changes: 7 additions & 0 deletions
7
test/rpc-integration/test-get-model/response-with-map-unsat2.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,7 @@ | ||
| { | ||
| "jsonrpc": "2.0", | ||
| "id": 1, | ||
| "result": { | ||
| "satisfiable": "Unsat" | ||
| } | ||
| } |
114 changes: 114 additions & 0 deletions
114
test/rpc-integration/test-get-model/response-with-map.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,114 @@ | ||
| { | ||
| "jsonrpc": "2.0", | ||
| "id": 1, | ||
| "result": { | ||
| "substitution": { | ||
| "format": "KORE", | ||
| "version": 1, | ||
| "term": { | ||
| "tag": "And", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortGeneratedTopCell", | ||
| "args": [] | ||
| }, | ||
| "patterns": [ | ||
| { | ||
| "tag": "Equals", | ||
| "argSort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| }, | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortGeneratedTopCell", | ||
| "args": [] | ||
| }, | ||
| "first": { | ||
| "tag": "EVar", | ||
| "name": "AMOUNT", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| } | ||
| }, | ||
| "second": { | ||
| "tag": "DV", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| }, | ||
| "value": "1" | ||
| } | ||
| }, | ||
| { | ||
| "tag": "Equals", | ||
| "argSort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| }, | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortGeneratedTopCell", | ||
| "args": [] | ||
| }, | ||
| "first": { | ||
| "tag": "EVar", | ||
| "name": "KEY", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| } | ||
| }, | ||
| "second": { | ||
| "tag": "DV", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortInt", | ||
| "args": [] | ||
| }, | ||
| "value": "0" | ||
| } | ||
| }, | ||
| { | ||
| "tag": "Equals", | ||
| "argSort": { | ||
| "tag": "SortApp", | ||
| "name": "SortMap", | ||
| "args": [] | ||
| }, | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortGeneratedTopCell", | ||
| "args": [] | ||
| }, | ||
| "first": { | ||
| "tag": "EVar", | ||
| "name": "Var'Ques'STORAGE", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortMap", | ||
| "args": [] | ||
| } | ||
| }, | ||
| "second": { | ||
| "tag": "EVar", | ||
| "name": "Var'Ques'STORAGE", | ||
| "sort": { | ||
| "tag": "SortApp", | ||
| "name": "SortMap", | ||
| "args": [] | ||
| } | ||
| } | ||
| } | ||
| ] | ||
| } | ||
| }, | ||
| "satisfiable": "Sat" | ||
| } | ||
| } |
Oops, something went wrong.