Make StrataCoreToGoto accept a user-specified Strata Core file #404
Conversation
It was previously hard-coded to a single test. Turn it into a workflow that accepts *.core.st files as command-line arguments.
There was a problem hiding this comment.
Pull request overview
Updates the StrataCoreToGoto executable so it can translate a user-specified Strata Core source file (*.core.st) into CBMC-compatible GOTO JSON outputs, instead of being hard-coded to the SimpleAdd test case.
Changes:
- Replace hard-coded SimpleAdd program import/entrypoint with a CLI that reads and elaborates a
.core.stfile. - Add basic CLI options (
--output-dir,--program-name) and derive default output names from the input filename. - Update the SimpleAdd CBMC helper script to invoke the new CLI form.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 4 comments.
| File | Description |
|---|---|
| StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh | Switches the script to call StrataCoreToGoto with an explicit input .core.st file and output directory. |
| StrataCoreToGoto.lean | Implements new CLI parsing, file loading/elaboration, and JSON output file naming for StrataCoreToGoto. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| let symTabFile := s!"{dir}/{programName}.symtab.json" | ||
| let gotoFile := s!"{dir}/{programName}.goto.json" | ||
| CoreToGOTO.writeToGotoJson (programName := programName) |
There was a problem hiding this comment.
The output paths are built via string concatenation ("{dir}/{programName}..."). If --program-name contains path separators or .., this can write outside --output-dir (path traversal / unintended overwrites). Consider validating programName to be a simple filename (no separators) and building paths with System.FilePath joins instead of hard-coded "/".
| let dir := opts.outputDir | ||
| let text ← Strata.Util.readInputSource file | ||
| let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file) | ||
| let dctx := Elab.LoadedDialects.builtin | ||
| let dctx := dctx.addDialect! Core | ||
| let leanEnv ← Lean.mkEmptyEnvironment 0 | ||
| match Strata.Elab.elabProgram dctx leanEnv inputCtx with | ||
| | .ok pgm => | ||
| let symTabFile := s!"{dir}/{programName}.symtab.json" | ||
| let gotoFile := s!"{dir}/{programName}.goto.json" | ||
| CoreToGOTO.writeToGotoJson (programName := programName) | ||
| (symTabFileName := symTabFile) | ||
| (gotoFileName := gotoFile) | ||
| pgm | ||
| IO.println s!"Written {symTabFile} and {gotoFile}" |
There was a problem hiding this comment.
--output-dir is not created before writing files; if the directory doesn't exist, IO.FS.writeFile will raise an exception and the tool will exit without a clean error message/exit code. Consider calling IO.FS.createDirAll on the output directory (or catching IO.Error around the write) and returning 1 with a helpful message when creation/writes fail.
tautschnig
changed the title
1 participant
Description of changes:
It was previously hard-coded to a single test. Turn it into a workflow that accepts a *.core.st file as command-line argument.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.