this repo has no description
fix(RS): Fix Rust backend crash on user record fields named `reference` or `trace` (#1982)
* Serialize QuintError.trace as #trace to avoid colliding with user record field names
* Replace recursive QuintError reviver with targeted reviveQuintError at known error sites
* Add regression test for #1981 covering user record fields named reference and trace
authored by
Yassine Boukhari
and committed by
GitHub
9d08bcf4
7efd6167
+51
-28
+2
evaluator/src/ir.rs
+2
evaluator/src/ir.rs
+10
quint/integration-tests/runtime/rust/run.md
+10
quint/integration-tests/runtime/rust/run.md
···
100
100
<!-- !test check 1736 -->
101
101
quint run --backend=rust testFixture/bug1736setOfMaps.qnt
102
102
103
+
### OK on run 1981
104
+
105
+
Regression test for [#1981](https://github.com/informalsystems/quint/issues/1981).
106
+
Tests that `quint run` works when user record fields are named `reference` or
107
+
`trace`, which used to collide with the Rust evaluator's QuintError JSON keys
108
+
and crash deserialization.
109
+
110
+
<!-- !test check 1981 -->
111
+
quint run --backend=rust testFixture/bug1981fieldNameCollision.qnt
112
+
103
113
### Run finds an invariant violation
104
114
105
115
The command `run` finds an invariant violation.
+11
-21
quint/src/jsonHelper.ts
+11
-21
quint/src/jsonHelper.ts
···
1
+
import { QuintError } from './quintError'
2
+
1
3
// Preprocess troublesome types so they are represented in JSON.
2
4
//
3
5
// We need it particularly because, by default, serialization of Map and Set
···
18
20
}
19
21
20
22
/**
21
-
* Reviver function for JSON.parse to ensure proper type conversions during deserialization.
22
-
*
23
-
* A "reviver" is the standard JavaScript term for the optional second parameter to JSON.parse(),
24
-
* which is called for each key-value pair during parsing, allowing transformation of values.
25
-
*
26
-
* This reviver ensures that:
27
-
* - QuintError.reference fields are converted from numbers to bigint
23
+
* Convert a QuintError parsed from the Rust evaluator's wire format into the
24
+
* TS-internal shape: rename `#trace` to `trace` and convert each id to bigint.
28
25
*
29
-
* @param key - The property key being parsed
30
-
* @param value - The parsed value
31
-
* @returns The potentially transformed value
32
-
*
33
-
* @see https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/JSON/parse#the_reviver_parameter
26
+
* Rust serializes the trace field as `#trace` so it cannot collide with user
27
+
* record fields named `trace` in the simulator output.
34
28
*/
35
-
export function reviver(key: string, value: any): any {
36
-
// Convert QuintError.reference from number to bigint (TS backend compatibility)
37
-
if (key === 'reference' && value !== null && value !== undefined) {
38
-
return BigInt(value)
39
-
}
40
-
// Convert QuintError.trace elements from number to bigint (Rust backend)
41
-
if (key === 'trace' && Array.isArray(value)) {
42
-
return value.map((v: any) => BigInt(v))
29
+
export function reviveQuintError(err: any): QuintError {
30
+
const { ['#trace']: trace, ...rest } = err
31
+
if (Array.isArray(trace)) {
32
+
return { ...rest, trace: trace.map((v: any) => BigInt(v)) }
43
33
}
44
-
return value
34
+
return rest
45
35
}
+7
-5
quint/src/rust/commandWrapper.ts
+7
-5
quint/src/rust/commandWrapper.ts
···
18
18
import { debugLog } from '../verbosity'
19
19
import JSONbig from 'json-bigint'
20
20
import { LookupDefinition, LookupTable } from '../names/base'
21
-
import { reviver } from '../jsonHelper'
21
+
import { reviveQuintError } from '../jsonHelper'
22
22
import { ItfState, ItfValue, diagnosticsOfItf, ofItf, pendingDiagnosticsOfItf } from '../itf'
23
23
import { Presets, SingleBar } from 'cli-progress'
24
24
import readline from 'readline'
···
114
114
const output = result.value
115
115
116
116
try {
117
-
const parsed: Outcome = JSONbig.parse(output, reviver)
117
+
const parsed: Outcome = JSONbig.parse(output)
118
+
parsed.errors = parsed.errors.map(reviveQuintError)
118
119
119
120
// Convert traces to ITF and ensure seed is bigint Note: When a
120
121
// SimulationError occurs in Rust, the error trace is included in
···
199
200
const output = result.value
200
201
201
202
try {
202
-
const parsed: TestResult = JSONbig.parse(output, reviver)
203
+
const parsed: TestResult = JSONbig.parse(output)
204
+
parsed.errors = parsed.errors.map(reviveQuintError)
203
205
204
206
// Convert seed to bigint
205
207
parsed.seed = BigInt(parsed.seed)
···
255
257
}
256
258
257
259
try {
258
-
const parsed = JSONbig.parse(result.value, reviver)
260
+
const parsed = JSONbig.parse(result.value)
259
261
const values: ItfValue[] = []
260
262
for (const r of parsed.results) {
261
263
if (r.error) {
262
-
return left(r.error)
264
+
return left(reviveQuintError(r.error))
263
265
}
264
266
values.push(r.value)
265
267
}
+5
-2
quint/src/rust/replServerWrapper.ts
+5
-2
quint/src/rust/replServerWrapper.ts
···
23
23
import { ChildProcess, spawn } from 'child_process'
24
24
import readline from 'readline'
25
25
import JSONbig from 'json-bigint'
26
-
import { reviver } from '../jsonHelper'
26
+
import { reviveQuintError } from '../jsonHelper'
27
27
import { bigintCheckerReplacer } from './helpers'
28
28
import { ofItfValue } from '../itf'
29
29
import { RuntimeValue, rv } from '../runtime/impl/runtimeValue'
···
151
151
152
152
this.stdout.on('line', (line: string) => {
153
153
try {
154
-
const response: ReplResponse = JSONbig.parse(line, reviver)
154
+
const response: ReplResponse = JSONbig.parse(line)
155
+
if ('err' in response && response.err) {
156
+
response.err = reviveQuintError(response.err)
157
+
}
155
158
156
159
if (response.response === 'FatalError') {
157
160
// Store the fatal error and shut down
+16
quint/testFixture/bug1981fieldNameCollision.qnt
+16
quint/testFixture/bug1981fieldNameCollision.qnt
···
1
+
module bug1981fieldNameCollision {
2
+
type Inner = { authority: int, round: int }
3
+
4
+
var data: { reference: Inner, trace: List[Inner] }
5
+
6
+
action init = {
7
+
data' = { reference: { authority: 0, round: 0 }, trace: [] }
8
+
}
9
+
10
+
action step = {
11
+
data' = {
12
+
reference: { authority: 1, round: data.reference.round + 1 },
13
+
trace: data.trace.append(data.reference),
14
+
}
15
+
}
16
+
}