Skip to content

Commit ef519ad

Browse files
author
Shon Feder
committed
Ensure transformations can't mutate the original object
There was some mutation happening via the transformer, which was wreaking havoc on attempts to complete #1298. Apparently it was also somehow leading to incorrect printing of sum type variants. I haven't had time to investigate why, but deep cloning the original object must be safer and it is fixing a blocking problem in ongoing work in #1298. Since the cases in which this causes problems are quite subtle, I havent been able to figure out how to test this directly.
1 parent 699219d commit ef519ad

File tree

4 files changed

+21
-28
lines changed

4 files changed

+21
-28
lines changed

quint/package.json

+4-12
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,7 @@
22
"name": "@informalsystems/quint",
33
"version": "0.18.3",
44
"description": "Core tool for the Quint specification language",
5-
"keywords": [
6-
"temporal",
7-
"logic",
8-
"formal",
9-
"specification",
10-
"verification"
11-
],
5+
"keywords": ["temporal", "logic", "formal", "specification", "verification"],
126
"homepage": "https://github.com/informalsystems/quint",
137
"bugs": "https://github.com/informalsystems/quint/issues",
148
"license": "Apache 2.0",
@@ -35,11 +29,7 @@
3529
"bin": {
3630
"quint": "dist/src/cli.js"
3731
},
38-
"files": [
39-
"README.md",
40-
"dist/**/*",
41-
"test/**/*.ts"
42-
],
32+
"files": ["README.md", "dist/**/*", "test/**/*.ts"],
4333
"engines": {
4434
"node": "18 - 20"
4535
},
@@ -63,6 +53,8 @@
6353
"line-column": "^1.0.2",
6454
"lodash": "^4.17.21",
6555
"lodash.isequal": "^4.5.0",
56+
"lodash.clonedeep": "4.5.0",
57+
"@types/lodash.clonedeep": "4.5.0",
6658
"seedrandom": "^3.0.5",
6759
"tar": "^6.1.14",
6860
"yargs": "^17.2.1"

quint/src/ir/IRTransformer.ts

+7-6
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import * as ir from './quintIr'
1717
import * as t from './quintTypes'
1818
import { unreachable } from '../util'
1919
import { LookupDefinition } from '../names/base'
20+
import cloneDeep from 'lodash.clonedeep'
2021

2122
export class IRTransformer {
2223
enterModule?: (module: ir.QuintModule) => ir.QuintModule
@@ -111,7 +112,7 @@ export class IRTransformer {
111112
* @returns the tranformed Quint module
112113
*/
113114
export function transformModule(transformer: IRTransformer, quintModule: ir.QuintModule): ir.QuintModule {
114-
let newModule = { ...quintModule }
115+
let newModule = cloneDeep(quintModule)
115116

116117
if (transformer.enterModule) {
117118
newModule = transformer.enterModule(newModule)
@@ -136,7 +137,7 @@ export function transformModule(transformer: IRTransformer, quintModule: ir.Quin
136137
* @returns the transformed Quint type
137138
*/
138139
export function transformType(transformer: IRTransformer, type: t.QuintType): t.QuintType {
139-
let newType = { ...type }
140+
let newType = cloneDeep(type)
140141
if (transformer.enterType) {
141142
newType = transformer.enterType(newType)
142143
}
@@ -317,7 +318,7 @@ export function transformLookupDefinition(transformer: IRTransformer, lud: Looku
317318
* @returns the transformed Quint definition
318319
*/
319320
export function transformDeclaration(transformer: IRTransformer, decl: ir.QuintDeclaration): ir.QuintDeclaration {
320-
let newDecl = { ...decl }
321+
let newDecl = cloneDeep(decl)
321322
if (transformer.enterDecl) {
322323
newDecl = transformer.enterDecl(newDecl)
323324
}
@@ -375,7 +376,7 @@ export function transformDeclaration(transformer: IRTransformer, decl: ir.QuintD
375376
* @returns the transformed Quint definition
376377
*/
377378
export function transformDefinition(transformer: IRTransformer, def: ir.QuintDef): ir.QuintDef {
378-
let newDef = { ...def }
379+
let newDef = cloneDeep(def)
379380
if (transformer.enterDef) {
380381
newDef = transformer.enterDef(newDef)
381382
}
@@ -450,7 +451,7 @@ export function transformDefinition(transformer: IRTransformer, def: ir.QuintDef
450451
* @returns the transformed Quint expression
451452
*/
452453
function transformExpression(transformer: IRTransformer, expr: ir.QuintEx): ir.QuintEx {
453-
let newExpr = { ...expr }
454+
let newExpr = cloneDeep(expr)
454455
if (transformer.enterExpr) {
455456
newExpr = transformer.enterExpr(newExpr)
456457
}
@@ -542,7 +543,7 @@ function transformExpression(transformer: IRTransformer, expr: ir.QuintEx): ir.Q
542543
* @returns the transformed Quint row
543544
*/
544545
export function transformRow(transformer: IRTransformer, row: t.Row): t.Row {
545-
let newRow = row
546+
let newRow = cloneDeep(row)
546547
if (transformer.enterRow) {
547548
newRow = transformer.enterRow(newRow)
548549
}

quint/test/ir/IRTransformer.test.ts

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
import { describe, it } from 'mocha'
22
import { assert } from 'chai'
33
import { buildModuleWithDecls } from '../builders/ir'
4-
import { QuintDeclaration, QuintDef, QuintEx, isDef } from '../../src/ir/quintIr'
4+
import { QuintDeclaration, QuintDef, QuintEx, isDef, QuintModule } from '../../src/ir/quintIr'
55
import { moduleToString } from '../../src/ir/IRprinting'
6-
import { IRTransformer, transformModule } from '../../src/ir/IRTransformer'
7-
import { ConcreteRow, QuintType } from '../../src/ir/quintTypes'
6+
import { IRTransformer, transformDeclaration, transformModule } from '../../src/ir/IRTransformer'
7+
import { ConcreteRow, QuintType, QuintVarType } from '../../src/ir/quintTypes'
88

99
const quintModule = buildModuleWithDecls([
1010
'var a: int',

quint/test/types/aliasInliner.test.ts

+7-7
Original file line numberDiff line numberDiff line change
@@ -70,13 +70,13 @@ describe('inlineAliases', () => {
7070
const { modules } = inlineModule(quintModule)
7171

7272
const expectedModule = dedent(`module A {
73-
| type T1 = (B({}) | C({}))
74-
| val C: (B({}) | C({})) = variant("C", Rec())
75-
| type T2 = (Some((B({}) | C({}))) | None({}))
76-
| val B: (B({}) | C({})) = variant("B", Rec())
77-
| def Some: ((B({}) | C({}))) => (Some((B({}) | C({}))) | None({})) = ((__SomeParam) => variant("Some", __SomeParam))
78-
| val None: (Some((B({}) | C({}))) | None({})) = variant("None", Rec())
79-
| var x: (Some((B({}) | C({}))) | None({}))
73+
| type T1 = (B | C)
74+
| val C: (B | C) = variant("C", Rec())
75+
| type T2 = (Some((B | C)) | None)
76+
| val B: (B | C) = variant("B", Rec())
77+
| def Some: ((B | C)) => (Some((B | C)) | None) = ((__SomeParam) => variant("Some", __SomeParam))
78+
| val None: (Some((B | C)) | None) = variant("None", Rec())
79+
| var x: (Some((B | C)) | None)
8080
|}`)
8181

8282
assert.deepEqual(moduleToString(modules[0]), expectedModule)

0 commit comments

Comments
 (0)