Merge pull request #1051 from informalsystems/gabriela/simulate-witho…

…ut-run-module

Remove wrapper `__run__` module from simulation

CHANGELOG.md

@@ -31,6 +31,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Do not fail on a bug in error formatting (#1063)
 - Fix unhandled error messages during parsing and typechecking on the Apalache
   server (#1074)
+- Fix a problem where some definitions would have to be exported from the
+  main module in order for the REPL and the simulator to load them (#1039 and #1051)
 
 ### Security
 

quint/cli-tests.md

@@ -278,13 +278,9 @@ fi
       --invariant=noBuyInDrawingInv --main=lotteryMempool \
       ../examples/solidity/icse23-fig7/lottery.qnt
 
-### IGNORE on run BinSearch10
+### OK on run BinSearch10
 
-This test should work, but due to a problem with flattening, it does not.
-Hence, we ignore it. When flattening is repaired, this test will start
-to work. Fix the exit code to 0 and IGNORE to OK.
-
-<!-- !test exit 1 -->
+<!-- !test exit 0 -->
 <!-- !test check BinSearch - Run -->
     quint run --max-samples=10000 --max-steps=10 \
       --invariant=Postcondition \

quint/src/IRprinting.ts

@@ -73,6 +73,9 @@ export function definitionToString(def: QuintDef, includeBody: boolean = true, t
       if (def.qualifiedName) {
         text += ` as ${def.qualifiedName}`
       }
+      if (def.fromSource) {
+        text += ` from "${def.fromSource}"`
+      }
       return text
     }
     case 'export': {
@@ -87,7 +90,16 @@ export function definitionToString(def: QuintDef, includeBody: boolean = true, t
     }
     case 'instance': {
       const overrides = def.overrides.map(o => `${o[0].name} = ${expressionToString(o[1])}`).join(', ')
-      return `import ${def.protoName}(${overrides}) as ${def.qualifiedName}`
+      let text = `import ${def.protoName}(${overrides})`
+      if (def.qualifiedName) {
+        text += ` as ${def.qualifiedName}`
+      } else {
+        text += `.*`
+      }
+      if (def.fromSource) {
+        text += ` from "${def.fromSource}"`
+      }
+      return text
     }
   }
 }

quint/src/cliCommands.ts

@@ -474,7 +474,10 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
   const startMs = Date.now()
 
   const mainPath = fileSourceResolver().lookupPath(dirname(prev.args.input), basename(prev.args.input))
-  const result = compileAndRun(newIdGenerator(), prev.sourceCode, mainName, mainPath, options)
+  const mainId = prev.modules.find(m => m.name === mainName)!.id
+  const mainStart = prev.sourceMap.get(mainId)!.start.index
+  const mainEnd = prev.sourceMap.get(mainId)!.end!.index
+  const result = compileAndRun(newIdGenerator(), prev.sourceCode, mainStart, mainEnd, mainName, mainPath, options)
 
   if (result.status === 'error') {
     const errors = prev.errors ? prev.errors.concat(result.errors) : result.errors

quint/src/simulation.ts

@@ -62,6 +62,8 @@ function errSimulationResult(status: SimulatorResultStatus, errors: ErrorMessage
  *
  * @param idGen a unique generator of identifiers
  * @param code the source code of the modules
+ * @param mainStart the start index of the main module in the code
+ * @param mainEnd the end index of the main module in the code
  * @param mainName the module that should be used as a state machine
  * @param mainPath the lookup path that was used to retrieve the main module
  * @param options simulator settings
@@ -71,6 +73,8 @@ function errSimulationResult(status: SimulatorResultStatus, errors: ErrorMessage
 export function compileAndRun(
   idGen: IdGenerator,
   code: string,
+  mainStart: number,
+  mainEnd: number,
   mainName: string,
   mainPath: SourceLookupPath,
   options: SimulatorOptions
@@ -82,23 +86,22 @@ export function compileAndRun(
   // that are required by the runner.
   // This code should be revisited in #618.
   const o = options
-  const wrappedCode = `${code}
+  // Defs required by the simulator, to be added to the main module before compilation
+  const extraDefs = [
+    `val ${lastTraceName} = [];`,
+    `def q::test(q::nrunsArg, q::nstepsArg, q::initArg, q::nextArg, q::invArg) = false`,
+    `action q::init = { ${o.init} }`,
+    `action q::step = { ${o.step} }`,
+    `val q::inv = { ${o.invariant} }`,
+    `val q::runResult = q::test(${o.maxSamples}, ${o.maxSteps}, q::init, q::step, q::inv)`,
+  ]
 
-module __run__ {
-  import ${mainName}.*
-
-  val ${lastTraceName} = [];
-  def q::test(q::nrunsArg, q::nstepsArg, q::initArg, q::nextArg, q::invArg) = false;
-  action q::init = { ${o.init} }
-  action q::step = { ${o.step} }
-  val q::inv = { ${o.invariant} }
-  val q::runResult =
-    q::test(${o.maxSamples}, ${o.maxSteps}, q::init, q::step, q::inv)
-}
-`
+  // Construct the modules' code, adding the extra definitions to the main module
+  const newMainModuleCode = code.slice(mainStart, mainEnd - 1) + extraDefs.join('\n')
+  const codeWithExtraDefs = code.slice(0, mainStart) + newMainModuleCode + code.slice(mainEnd)
 
   const recorder = newTraceRecorder(options.verbosity, options.rng)
-  const ctx = compileFromCode(idGen, wrappedCode, '__run__', mainPath, recorder, options.rng.next)
+  const ctx = compileFromCode(idGen, codeWithExtraDefs, mainName, mainPath, recorder, options.rng.next)
 
   if (ctx.compileErrors.length > 0 || ctx.syntaxErrors.length > 0 || ctx.analysisErrors.length > 0) {
     const errors = ctx.syntaxErrors.concat(ctx.analysisErrors).concat(ctx.compileErrors)

quint/test/IRprinting.test.ts

@@ -65,12 +65,60 @@ describe('definitionToString', () => {
     assert.deepEqual(definitionToString(def), expectedDef)
   })
 
+  it('pretty prints import definitions with qualifier', () => {
+    const def = buildDef('import M as M1')
+    const expectedDef = 'import M as M1'
+    assert.deepEqual(definitionToString(def), expectedDef)
+  })
+
+  it('pretty prints import definitions with the module name as qualifier', () => {
+    const def = buildDef('import M')
+    const expectedDef = 'import M'
+    assert.deepEqual(definitionToString(def), expectedDef)
+  })
+
+  it('pretty prints import definitions with from statement', () => {
+    const def = buildDef('import M.* from "./file"')
+    const expectedDef = 'import M.* from "./file"'
+    assert.deepEqual(definitionToString(def), expectedDef)
+  })
+
   it('pretty prints instance definitions', () => {
+    const def = buildDef('import M(x = N + 1, y = 3).*')
+    const expectedDef = 'import M(x = iadd(N, 1), y = 3).*'
+    assert.deepEqual(definitionToString(def), expectedDef)
+  })
+
+  it('pretty prints instance definitions with qualifier', () => {
     const def = buildDef('import M(x = N + 1, y = 3) as A')
     const expectedDef = 'import M(x = iadd(N, 1), y = 3) as A'
     assert.deepEqual(definitionToString(def), expectedDef)
   })
 
+  it('pretty prints instance definitions with from statement', () => {
+    const def = buildDef('import M(x = N + 1, y = 3) as A from "./file"')
+    const expectedDef = 'import M(x = iadd(N, 1), y = 3) as A from "./file"'
+    assert.deepEqual(definitionToString(def), expectedDef)
+  })
+
+  it('pretty prints export definitions', () => {
+    const def = buildDef('export M.*')
+    const expectedDef = 'export M.*'
+    assert.deepEqual(definitionToString(def), expectedDef)
+  })
+
+  it('pretty prints export definitions with qualifier', () => {
+    const def = buildDef('export M as M1')
+    const expectedDef = 'export M as M1'
+    assert.deepEqual(definitionToString(def), expectedDef)
+  })
+
+  it('pretty prints export definitions with the module name as qualifier', () => {
+    const def = buildDef('export M')
+    const expectedDef = 'export M'
+    assert.deepEqual(definitionToString(def), expectedDef)
+  })
+
   it('pretty prints definitions with given type', () => {
     const def = buildDef('val f = 1')
     const expectedDef = 'val f: int = 1'