1
1
mirror of https://github.com/anoma/juvix.git synced 2024-11-30 14:13:27 +03:00

CASM serialization (#2679)

* Closes #2563 

Checklist
------------

- [x] Serialization of the Haskell CASM representation to the JSON
format accepted by the Cairo VM.
- [x] Add the `cairo` target to the `compile` commands.
- [x] Output via the Cairo `output` builtin.
- [x] Relativize jumps. Cairo VM doesn't actually support absolute
jumps.
- [x] Test the translation from CASM to Cairo by running the output in
the Cairo VM
- [x] Add Cairo VM to the CI
This commit is contained in:
Łukasz Czajka 2024-03-26 17:18:52 +01:00 committed by GitHub
parent 29f1c4c4df
commit 7d559b1f18
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
56 changed files with 1416 additions and 359 deletions

View File

@ -92,6 +92,7 @@ jobs:
- name: Add ~/.local/bin to PATH
run: |
mkdir -p "$HOME/.local/bin"
echo "$HOME/.local/bin" >> $GITHUB_PATH
- name: Install the latest Wasmer version
@ -118,6 +119,19 @@ jobs:
run: |
vamp-ir --version
- name: Install Rust toolchain
uses: actions-rust-lang/setup-rust-toolchain@v1
- name: Install Cairo VM
shell: bash
run: |
git clone https://github.com/lambdaclass/cairo-vm.git
cd cairo-vm
cargo build --release
cp target/release/cairo-vm-cli $HOME/.local/bin/cairo-vm-cli
cd -
cp main/scripts/run_cairo_vm.sh $HOME/.local/bin/run_cairo_vm.sh
- name: Make runtime
run: |
cd main
@ -274,6 +288,26 @@ jobs:
echo "CC=$(brew --prefix llvm@15)/bin/clang" >> $GITHUB_ENV
echo "LIBTOOL=$(brew --prefix llvm@15)/bin/llvm-ar" >> $GITHUB_ENV
- name: Add ~/.local/bin to PATH
run: |
mkdir -p "$HOME/.local/bin"
echo "$HOME/.local/bin" >> $GITHUB_PATH
- name: Install Rust toolchain
uses: actions-rust-lang/setup-rust-toolchain@v1
- name: Install Cairo VM
shell: bash
run: |
git clone https://github.com/lambdaclass/cairo-vm.git
cd cairo-vm
cargo build --release
cp -a target/release/cairo-vm-cli $HOME/.local/bin/cairo-vm-cli
chmod a+x $HOME/.local/bin/cairo-vm-cli
cd -
cp -a main/scripts/run_cairo_vm.sh $HOME/.local/bin/run_cairo_vm.sh
chmod a+x $HOME/.local/bin/run_cairo_vm.sh
- name: Make runtime
run: |
cd main
@ -325,10 +359,6 @@ jobs:
make CC=$CC LIBTOOL=$LIBTOOL install
make CC=$CC LIBTOOL=$LIBTOOL test
- name: Add ~/.local/bin to PATH
run: |
echo "$HOME/.local/bin" >> $GITHUB_PATH
- name: Typecheck and format Juvix examples
if: ${{ success() }}
shell: bash

View File

@ -29,6 +29,7 @@ runCommand opts@CompileOptions {..} = do
TargetReg -> Compile.runRegPipeline arg
TargetAnoma -> Compile.runAnomaPipeline arg
TargetCasm -> Compile.runCasmPipeline arg
TargetCairo -> Compile.runCairoPipeline arg
writeCoreFile :: (Members '[EmbedIO, App, TaggedLock] r) => Compile.PipelineArg -> Sem r ()
writeCoreFile pa@Compile.PipelineArg {..} = do

View File

@ -3,6 +3,7 @@ module Commands.Dev.Asm.Compile where
import Commands.Base
import Commands.Dev.Asm.Compile.Options
import Commands.Extra.Compile qualified as Compile
import Data.Aeson qualified as JSON
import Juvix.Compiler.Asm.Translation.FromSource qualified as Asm
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.C qualified as C
@ -46,6 +47,15 @@ runCommand opts = do
$ tab
Casm.Result {..} <- getRight r
writeFileEnsureLn casmFile (toPlainText $ Casm.ppProgram _resultCode)
TargetCairo -> do
cairoFile <- Compile.outputFile opts file
r <-
runReader entryPoint
. runError @JuvixError
. asmToCairo
$ tab
res <- getRight r
liftIO $ JSON.encodeFile (toFilePath cairoFile) res
_ ->
case run $ runReader entryPoint $ runError $ asmToMiniC tab of
Left err -> exitJuvixError err
@ -70,6 +80,7 @@ runCommand opts = do
TargetNative64 -> return Backend.TargetCNative64
TargetReg -> return Backend.TargetReg
TargetCasm -> return Backend.TargetCairo
TargetCairo -> return Backend.TargetCairo
TargetAnoma -> err "Anoma"
TargetTree -> err "JuvixTree"
TargetGeb -> err "GEB"

View File

@ -16,7 +16,8 @@ asmSupportedTargets =
[ TargetWasm32Wasi,
TargetNative64,
TargetReg,
TargetCasm
TargetCasm,
TargetCairo
]
parseAsmCompileOptions :: Parser AsmCompileOptions

View File

@ -1,11 +1,13 @@
module Commands.Dev.Casm where
import Commands.Base
import Commands.Dev.Casm.Compile as Compile
import Commands.Dev.Casm.Options
import Commands.Dev.Casm.Read as Read
import Commands.Dev.Casm.Run as Run
runCommand :: forall r. (Members '[EmbedIO, App, TaggedLock] r) => CasmCommand -> Sem r ()
runCommand = \case
Compile opts -> Compile.runCommand opts
Run opts -> Run.runCommand opts
Read opts -> Read.runCommand opts

View File

@ -0,0 +1,57 @@
module Commands.Dev.Casm.Compile where
import Commands.Base
import Commands.Dev.Casm.Compile.Options
import Commands.Extra.Compile qualified as Compile
import Data.Aeson qualified as JSON
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Casm.Data.Result qualified as Casm
import Juvix.Compiler.Casm.Translation.FromSource qualified as Casm
import Juvix.Compiler.Casm.Validate qualified as Casm
runCommand :: forall r. (Members '[EmbedIO, App, TaggedLock] r) => CompileOptions -> Sem r ()
runCommand opts = do
file <- getFile
s <- readFile file
case Casm.runParser file s of
Left err -> exitJuvixError (JuvixError err)
Right (labi, code) ->
case Casm.validate labi code of
Left err -> exitJuvixError (JuvixError err)
Right () -> do
ep <- getEntryPoint (AppPath (preFileFromAbs file) True)
tgt <- getTarget (opts ^. compileTarget)
let entryPoint :: EntryPoint
entryPoint =
ep
{ _entryPointTarget = tgt,
_entryPointDebug = opts ^. compileDebug
}
cairoFile <- Compile.outputFile opts file
r <-
runReader entryPoint
. runError @JuvixError
. casmToCairo
$ Casm.Result labi code
res <- getRight r
liftIO $ JSON.encodeFile (toFilePath cairoFile) res
where
getFile :: Sem r (Path Abs File)
getFile = getMainFile (opts ^. compileInputFile)
getTarget :: CompileTarget -> Sem r Backend.Target
getTarget = \case
TargetCairo -> return Backend.TargetCairo
TargetWasm32Wasi -> err "WASM"
TargetNative64 -> err "native"
TargetCasm -> err "CASM"
TargetReg -> err "JuvixReg"
TargetAnoma -> err "Anoma"
TargetTree -> err "JuvixTree"
TargetGeb -> err "GEB"
TargetVampIR -> err "VampIR"
TargetCore -> err "JuvixCore"
TargetAsm -> err "JuvixAsm"
where
err :: Text -> Sem r a
err tgt = exitMsg (ExitFailure 1) ("error: " <> tgt <> " target not supported for CASM")

View File

@ -0,0 +1,21 @@
module Commands.Dev.Casm.Compile.Options
( module Commands.Dev.Casm.Compile.Options,
module Commands.Extra.Compile.Options,
)
where
import Commands.Extra.Compile.Options
import CommonOptions
import Data.List.NonEmpty qualified as NonEmpty
casmSupportedTargets :: NonEmpty CompileTarget
casmSupportedTargets =
NonEmpty.fromList
[ TargetCairo
]
parseCasmCompileOptions :: Parser CompileOptions
parseCasmCompileOptions =
parseCompileOptions
casmSupportedTargets
(parseInputFile FileExtCasm)

View File

@ -1,11 +1,13 @@
module Commands.Dev.Casm.Options where
import Commands.Dev.Casm.Compile.Options
import Commands.Dev.Casm.Read.Options
import Commands.Dev.Casm.Run.Options
import CommonOptions
data CasmCommand
= Run CasmRunOptions
= Compile CompileOptions
| Run CasmRunOptions
| Read CasmReadOptions
deriving stock (Data)
@ -13,16 +15,26 @@ parseCasmCommand :: Parser CasmCommand
parseCasmCommand =
hsubparser $
mconcat
[ commandRun,
[ commandCompile,
commandRun,
commandRead
]
where
commandCompile :: Mod CommandFields CasmCommand
commandCompile = command "compile" compileInfo
commandRun :: Mod CommandFields CasmCommand
commandRun = command "run" runInfo
commandRead :: Mod CommandFields CasmCommand
commandRead = command "read" readInfo
compileInfo :: ParserInfo CasmCommand
compileInfo =
info
(Compile <$> parseCasmCompileOptions)
(progDesc "Compile a CASM file")
runInfo :: ParserInfo CasmCommand
runInfo =
info

View File

@ -23,6 +23,7 @@ runCommand opts = do
TargetTree -> runTreePipeline arg
TargetAnoma -> runAnomaPipeline arg
TargetCasm -> runCasmPipeline arg
TargetCairo -> runCairoPipeline arg
where
getFile :: Sem r (Path Abs File)
getFile = getMainFile (opts ^. compileInputFile)

View File

@ -4,6 +4,7 @@ import Commands.Base
import Commands.Dev.Core.Compile.Options
import Commands.Dev.Tree.Compile.Base (outputAnomaResult)
import Commands.Extra.Compile qualified as Compile
import Data.Aeson qualified as JSON
import Juvix.Compiler.Asm.Pretty qualified as Asm
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.C qualified as C
@ -48,6 +49,7 @@ getEntry PipelineArg {..} = do
TargetTree -> Backend.TargetTree
TargetAnoma -> Backend.TargetAnoma
TargetCasm -> Backend.TargetCairo
TargetCairo -> Backend.TargetCairo
defaultOptLevel :: Int
defaultOptLevel
@ -169,3 +171,15 @@ runCasmPipeline pa@PipelineArg {..} = do
$ _pipelineArgModule
Casm.Result {..} <- getRight r
writeFileEnsureLn casmFile (toPlainText $ Casm.ppProgram _resultCode)
runCairoPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
runCairoPipeline pa@PipelineArg {..} = do
entryPoint <- getEntry pa
cairoFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
r <-
runReader entryPoint
. runError @JuvixError
. coreToCairo
$ _pipelineArgModule
res <- getRight r
liftIO $ JSON.encodeFile (toFilePath cairoFile) res

View File

@ -13,14 +13,15 @@ type CoreCompileOptions = CompileOptions
coreSupportedTargets :: NonEmpty CompileTarget
coreSupportedTargets =
NonEmpty.fromList
[ TargetWasm32Wasi,
TargetNative64,
[ TargetNative64,
TargetWasm32Wasi,
TargetGeb,
TargetVampIR,
TargetTree,
TargetAsm,
TargetReg,
TargetCasm
TargetCasm,
TargetCairo
]
parseCoreCompileOptions :: Parser CoreCompileOptions

View File

@ -3,6 +3,7 @@ module Commands.Dev.Reg.Compile where
import Commands.Base
import Commands.Dev.Reg.Compile.Options
import Commands.Extra.Compile qualified as Compile
import Data.Aeson qualified as JSON
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.C qualified as C
import Juvix.Compiler.Casm.Data.Result qualified as Casm
@ -35,6 +36,15 @@ runCommand opts = do
$ tab
Casm.Result {..} <- getRight r
writeFileEnsureLn casmFile (toPlainText $ Casm.ppProgram _resultCode)
TargetCairo -> do
cairoFile <- Compile.outputFile opts file
r <-
runReader entryPoint
. runError @JuvixError
. regToCairo
$ tab
res <- getRight r
liftIO $ JSON.encodeFile (toFilePath cairoFile) res
_ ->
case run $ runReader entryPoint $ runError $ regToMiniC tab of
Left err -> exitJuvixError err
@ -58,6 +68,7 @@ runCommand opts = do
TargetWasm32Wasi -> return Backend.TargetCWasm32Wasi
TargetNative64 -> return Backend.TargetCNative64
TargetCasm -> return Backend.TargetCairo
TargetCairo -> return Backend.TargetCairo
TargetReg -> err "JuvixReg"
TargetAnoma -> err "Anoma"
TargetTree -> err "JuvixTree"

View File

@ -11,9 +11,10 @@ import Data.List.NonEmpty qualified as NonEmpty
regSupportedTargets :: NonEmpty CompileTarget
regSupportedTargets =
NonEmpty.fromList
[ TargetWasm32Wasi,
TargetNative64,
TargetCasm
[ TargetNative64,
TargetWasm32Wasi,
TargetCasm,
TargetCairo
]
parseRegCompileOptions :: Parser CompileOptions

View File

@ -11,8 +11,8 @@ newtype RuntimeCommand
runtimeSupportedTargets :: NonEmpty CompileTarget
runtimeSupportedTargets =
NonEmpty.fromList
[ TargetWasm32Wasi,
TargetNative64
[ TargetNative64,
TargetWasm32Wasi
]
parseRuntimeOptions :: Parser CompileOptions

View File

@ -22,6 +22,7 @@ runCommand opts = do
TargetTree -> return ()
TargetAnoma -> runAnomaPipeline arg
TargetCasm -> runCasmPipeline arg
TargetCairo -> runCairoPipeline arg
where
getFile :: Sem r (Path Abs File)
getFile = getMainFile (opts ^. compileInputFile)

View File

@ -3,6 +3,7 @@ module Commands.Dev.Tree.Compile.Base where
import Commands.Base
import Commands.Dev.Tree.Compile.Options
import Commands.Extra.Compile qualified as Compile
import Data.Aeson qualified as JSON
import Juvix.Compiler.Asm.Pretty qualified as Asm
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.C qualified as C
@ -44,6 +45,7 @@ getEntry PipelineArg {..} = do
TargetTree -> Backend.TargetTree
TargetAnoma -> Backend.TargetAnoma
TargetCasm -> Backend.TargetCairo
TargetCairo -> Backend.TargetCairo
defaultOptLevel :: Int
defaultOptLevel
@ -134,3 +136,15 @@ runCasmPipeline pa@PipelineArg {..} = do
$ _pipelineArgTable
Casm.Result {..} <- getRight r
writeFileEnsureLn casmFile (toPlainText $ Casm.ppProgram _resultCode)
runCairoPipeline :: (Members '[EmbedIO, App, TaggedLock] r) => PipelineArg -> Sem r ()
runCairoPipeline pa@PipelineArg {..} = do
entryPoint <- getEntry pa
cairoFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
r <-
runReader entryPoint
. runError @JuvixError
. treeToCairo
$ _pipelineArgTable
res <- getRight r
liftIO $ JSON.encodeFile (toFilePath cairoFile) res

View File

@ -10,11 +10,12 @@ import CommonOptions
treeSupportedTargets :: NonEmpty CompileTarget
treeSupportedTargets =
nonEmpty'
[ TargetWasm32Wasi,
TargetNative64,
[ TargetNative64,
TargetWasm32Wasi,
TargetAsm,
TargetReg,
TargetCasm,
TargetCairo,
TargetAnoma
]

View File

@ -37,6 +37,7 @@ runCompile inputFile o = do
TargetTree -> return (Right ())
TargetAnoma -> return (Right ())
TargetCasm -> return (Right ())
TargetCairo -> return (Right ())
prepareRuntime :: forall r. (Members '[App, EmbedIO] r) => Path Abs Dir -> CompileOptions -> Sem r ()
prepareRuntime buildDir o = do
@ -56,6 +57,7 @@ prepareRuntime buildDir o = do
TargetTree -> return ()
TargetAnoma -> return ()
TargetCasm -> return ()
TargetCairo -> return ()
where
wasiReleaseRuntime :: BS.ByteString
wasiReleaseRuntime = $(FE.makeRelativeToProject "runtime/_build.wasm32-wasi/libjuvix.a" >>= FE.embedFile)
@ -121,6 +123,8 @@ outputFile opts inputFile =
replaceExtension' nockmaFileExt baseOutputFile
TargetCasm ->
replaceExtension' casmFileExt baseOutputFile
TargetCairo ->
replaceExtension' jsonFileExt baseOutputFile
clangNativeCompile ::
forall r.

View File

@ -5,8 +5,8 @@ import Juvix.Compiler.Pipeline.EntryPoint
import Prelude (Show (show))
data CompileTarget
= TargetWasm32Wasi
| TargetNative64
= TargetNative64
| TargetWasm32Wasi
| TargetGeb
| TargetVampIR
| TargetCore
@ -15,6 +15,7 @@ data CompileTarget
| TargetTree
| TargetAnoma
| TargetCasm
| TargetCairo
deriving stock (Eq, Data, Bounded, Enum)
instance Show CompileTarget where
@ -29,6 +30,7 @@ instance Show CompileTarget where
TargetTree -> "tree"
TargetAnoma -> "anoma"
TargetCasm -> "casm"
TargetCairo -> "cairo"
data CompileOptions = CompileOptions
{ _compileDebug :: Bool,
@ -134,7 +136,7 @@ optCompileTarget supportedTargets =
( long "target"
<> short 't'
<> metavar "TARGET"
<> value TargetNative64
<> value (head supportedTargets)
<> showDefault
<> help ("select a target: " <> show listTargets)
<> completeWith (map show listTargets)

View File

@ -1,26 +1,102 @@
-- Juvix runtime for Cairo assembly
-- Closure layout: [ addr | 9 - sargs | 9 - argsnum | arguments... ]
-- Closure layout: [ fuid | 9 - sargs | 9 - argsnum | arguments... ]
-- fuid -- function id which also indicates the relative jump
-- offset for closure call (see juvix_call_closure below)
-- sargs -- number of arguments stored in the closure
-- argsnum -- number of arguments left
-- sargs + argsnum = total numer of arguments for the function
-- Maximum number of function arguments: 8
-- after calling juvix_get_regs:
-- [ap - 4] == fp
-- [ap - 3] == pc
-- [ap - 2] == ap - 2
-- [ap - 4] = fp
-- [ap - 3] = pc
-- [ap - 2] = ap - 2
juvix_get_regs:
call juvix_get_ap_reg
ret
juvix_get_ap_reg:
ret
-- [fp - 3]: closure
-- [fp - 4]: n = the number of arguments to extend with
-- [fp - 4 - k]: argument n - k - 1 (reverse order!)
juvix_extend_closure:
-- copy stored args reversing them;
-- to copy the stored args to the new closure
-- we need to jump forward, so the stored args
-- need to be available at consecutive memory
-- addresses backwards
jmp rel [[fp - 3] + 1]
[ap] = [[fp - 3] + 10]; ap++
[ap] = [[fp - 3] + 9]; ap++
[ap] = [[fp - 3] + 8]; ap++
[ap] = [[fp - 3] + 7]; ap++
[ap] = [[fp - 3] + 6]; ap++
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
-- the following ensures continuous memory use
-- with a compile-time contant offset for local
-- variables
[ap] = 10; ap++
[ap] = [[fp - 3] + 1]; ap++
[ap] = [ap - 2] - [ap - 1]; ap++
jmp rel [ap - 1]
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
-- now ap = fp + 11
-- alloc
call juvix_get_regs
-- now ap = fp + 15
-- [fp + 15] = pointer to new closure
[ap] = [ap - 2] + 8; ap++
-- [fp + 16] = 9 - sargs
[ap] = [[fp - 3] + 1]; ap++
-- [fp + 17] = 9 - argsnum (expected)
[ap] = [[fp - 3] + 2]; ap++
-- [fp + 18] = 9
[ap] = 9; ap++
-- [fp + 19] = sargs
[ap] = [fp + 18] - [fp + 16]; ap++
-- [fp + 20] = 9 - n
[ap] = [fp + 18] - [fp - 4]; ap++
-- closure header
[ap] = [[fp - 3]]; ap++
[ap] = [fp + 16] - [fp - 4]; ap++
[ap] = [fp + 17] + [fp - 4]; ap++
-- copy stored args: jmp rel (9 - sargs)
jmp rel [fp + 16]
[ap] = [fp + 7]; ap++
[ap] = [fp + 6]; ap++
[ap] = [fp + 5]; ap++
[ap] = [fp + 4]; ap++
[ap] = [fp + 3]; ap++
[ap] = [fp + 2]; ap++
[ap] = [fp + 1]; ap++
[ap] = [fp]; ap++
-- copy extra args: jmp rel (9 - extra args num)
jmp rel [fp + 20]
[ap] = [fp - 12]; ap++
[ap] = [fp - 11]; ap++
[ap] = [fp - 10]; ap++
[ap] = [fp - 9]; ap++
[ap] = [fp - 8]; ap++
[ap] = [fp - 7]; ap++
[ap] = [fp - 6]; ap++
[ap] = [fp - 5]; ap++
-- return value
[ap] = [fp + 15]; ap++
ret
-- [fp - 3]: closure; [fp - 3 - k]: argument k to closure call
juvix_call_closure:
ap += 1
-- closure addr
[fp] = [[fp - 3]]
-- jmp rel (9 - argsnum)
jmp rel [[fp - 3] + 2]
[ap] = [fp - 11]; ap++
@ -41,59 +117,7 @@ juvix_call_closure:
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call [fp]
ret
-- [fp - 3]: closure
-- [fp - 4]: n = the number of arguments to extend with
-- [fp - 4 - k]: argument n - k - 1 (reverse order!)
juvix_extend_closure:
ap += 6
-- 9 - sargs
[fp + 1] = [[fp - 3] + 1]
-- 9 - argsnum (expected)
[fp + 2] = [[fp - 3] + 2]
[fp + 3] = 9
-- [fp + 4] = sargs
[fp + 4] = [fp + 3] - [fp + 1]
-- [fp + 5] = 9 - n
[fp + 5] = [fp + 3] - [fp - 4]
-- copy stored args reversing them
jmp rel [fp + 1]
[ap] = [[fp - 3] + 10]; ap++
[ap] = [[fp - 3] + 9]; ap++
[ap] = [[fp - 3] + 8]; ap++
[ap] = [[fp - 3] + 7]; ap++
[ap] = [[fp - 3] + 6]; ap++
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call juvix_get_regs
[fp] = [ap - 2] + 2
-- closure header
[ap] = [[fp - 3]]; ap++
[ap] = [fp + 1] - [fp - 4]; ap++
[ap] = [fp + 2] + [fp - 4]; ap++
-- copy stored args: jmp rel (9 - sargs)
jmp rel [fp + 1]
[ap] = [fp + 13]; ap++
[ap] = [fp + 12]; ap++
[ap] = [fp + 11]; ap++
[ap] = [fp + 10]; ap++
[ap] = [fp + 9]; ap++
[ap] = [fp + 8]; ap++
[ap] = [fp + 7]; ap++
[ap] = [fp + 6]; ap++
-- copy extra args: jmp rel (9 - extra args num)
jmp rel [fp + 5]
[ap] = [fp - 12]; ap++
[ap] = [fp - 11]; ap++
[ap] = [fp - 10]; ap++
[ap] = [fp - 9]; ap++
[ap] = [fp - 8]; ap++
[ap] = [fp - 7]; ap++
[ap] = [fp - 6]; ap++
[ap] = [fp - 5]; ap++
-- return value
[ap] = [fp]; ap++
ret
jmp rel [[fp - 3]]
-- The above jump needs to be the last instruction in this file.
-- Calls to all possible functions are appended here by the
-- JuvixReg to CASM translation.

45
scripts/gen_stone_params.py Executable file
View File

@ -0,0 +1,45 @@
#!/usr/bin/env python
#
# This script generates appropriate Stone prover parameters with the right
# bounds for the number of execution steps.
#
# Invocation: gen_stone_params.py prog_public_input.json
#
import json
import sys
import math
if len(sys.argv) != 2:
sys.exit("Usage: gen_stone_params.py prog_public_input.json")
f = open(sys.argv[1])
data = json.load(f)
f.close()
n = int(math.log2(data["n_steps"])) - 6
if n < 0:
sys.exit("Too few execution steps (at least 64 required)")
fri_step_list = [0, 4]
while n > 3:
fri_step_list.append(3)
n -= 3
if n > 0:
fri_step_list.append(n)
out = {
"field": "PrimeField0",
"stark": {
"fri": {
"fri_step_list": fri_step_list,
"last_layer_degree_bound": 64,
"n_queries": 18,
"proof_of_work_bits": 24,
},
"log_n_cosets": 4,
},
"use_extension_field": False,
}
print(json.dumps(out))

5
scripts/run_cairo_vm.sh Executable file
View File

@ -0,0 +1,5 @@
#!/usr/bin/env bash
BASE=`basename "$1" .json`
cairo-vm-cli "$1" --print_output --proof_mode --trace_file ${BASE}.trace --air_public_input=${BASE}_public_input.json --air_private_input=${BASE}_private_input.json --memory_file=${BASE}_memory.mem --layout=small

6
scripts/run_stone_prover.sh Executable file
View File

@ -0,0 +1,6 @@
#!/usr/bin/env bash
BASE=`basename "$1" .json`
gen_stone_params.py ${BASE}_public_input.json > ${BASE}_params.json
cpu_air_prover --out_file=${BASE}_proof.json --private_input_file=${BASE}_private_input.json --public_input_file=${BASE}_public_input.json --prover_config_file=cpu_air_prover_config.json --parameter_file=${BASE}_params.json

View File

@ -0,0 +1,12 @@
module Juvix.Compiler.Backend.Cairo
( module Juvix.Compiler.Backend.Cairo.Data.Result,
module Juvix.Compiler.Backend.Cairo.Extra.Serialization,
module Juvix.Compiler.Backend.Cairo.Translation.FromCasm,
module Juvix.Compiler.Backend.Cairo.Language,
)
where
import Juvix.Compiler.Backend.Cairo.Data.Result
import Juvix.Compiler.Backend.Cairo.Extra.Serialization
import Juvix.Compiler.Backend.Cairo.Language
import Juvix.Compiler.Backend.Cairo.Translation.FromCasm

View File

@ -0,0 +1,48 @@
module Juvix.Compiler.Backend.Cairo.Data.Result where
import Data.Aeson as Aeson hiding (Result)
import Juvix.Prelude hiding ((.=))
data Result = Result
{ _resultData :: [Text],
_resultStart :: Int,
_resultEnd :: Int,
_resultMain :: Int,
_resultBuiltins :: [Text]
}
makeLenses ''Result
instance ToJSON Result where
toJSON Result {..} =
object
[ "data" .= toJSON _resultData,
"attributes" .= Array mempty,
"builtins" .= toJSON _resultBuiltins,
"hints" .= object [],
"identifiers"
.= object
[ "__main__.__start__"
.= object
[ "pc" .= Number (fromIntegral _resultStart),
"type" .= String "label"
],
"__main__.__end__"
.= object
[ "pc" .= Number (fromIntegral _resultEnd),
"type" .= String "label"
],
"__main__.main"
.= object
[ "pc" .= Number (fromIntegral _resultMain),
"decorators" .= Array mempty,
"type" .= String "function"
]
],
"main_scope" .= String "__main__",
"prime" .= String "0x800000000000011000000000000000000000000000000000000000000000001",
"reference_manager"
.= object
[ "references" .= Array mempty
]
]

View File

@ -0,0 +1,104 @@
module Juvix.Compiler.Backend.Cairo.Extra.Serialization where
import Data.Bits
import Juvix.Compiler.Backend.Cairo.Data.Result
import Juvix.Compiler.Backend.Cairo.Language
import Numeric
serialize :: [Element] -> Result
serialize elems =
Result
{ _resultData =
initializeOutput
++ map toHexText (serialize' elems)
++ finalizeOutput
++ finalizeJump,
_resultStart = 0,
_resultEnd = length initializeOutput + length elems + length finalizeOutput,
_resultMain = 0,
_resultBuiltins = ["output"]
}
where
toHexText :: Natural -> Text
toHexText n = "0x" <> fromString (showHex n "")
initializeOutput :: [Text]
initializeOutput =
[ "0x40480017fff7fff",
"0x1"
]
finalizeOutput :: [Text]
finalizeOutput =
[ "0x4002800080007fff",
"0x4826800180008000",
"0x1"
]
finalizeJump :: [Text]
finalizeJump =
[ "0x10780017fff7fff",
"0x0"
]
serialize' :: [Element] -> [Natural]
serialize' = map goElement
where
goElement :: Element -> Natural
goElement = \case
ElementInstruction i -> goInstr i
ElementImmediate f -> fieldToNatural f
goInstr :: Instruction -> Natural
goInstr Instruction {..} =
toBiasedRepr _instrOffDst
.|. shift (toBiasedRepr _instrOffOp0) 16
.|. shift (toBiasedRepr _instrOffOp1) 32
.|. shift (goReg _instrDstReg) 48
.|. shift (goReg _instrOp0Reg) 49
.|. shift (goOp1Src _instrOp1Src) 50
.|. shift (goResLogic _instrResLogic) 53
.|. shift (goPcUpdate _instrPcUpdate) 55
.|. shift (goApUpdate _instrApUpdate) 58
.|. shift (goOpcode _instrOpcode) 60
toBiasedRepr :: Offset -> Natural
toBiasedRepr off = fromIntegral (fromIntegral @Int16 @Integer off + (2 :: Integer) ^ (15 :: Integer))
goReg :: Reg -> Natural
goReg = \case
Ap -> 0
Fp -> 1
goOp1Src :: Op1Src -> Natural
goOp1Src = \case
Op1SrcOp0 -> 0
Op1SrcImm -> 1
Op1SrcFp -> 2
Op1SrcAp -> 4
goResLogic :: ResLogic -> Natural
goResLogic = \case
ResOp1 -> 0
ResAdd -> 1
ResMul -> 2
goPcUpdate :: PcUpdate -> Natural
goPcUpdate = \case
PcUpdateRegular -> 0
PcUpdateJump -> 1
PcUpdateJumpRel -> 2
PcUpdateJnz -> 4
goApUpdate :: ApUpdate -> Natural
goApUpdate = \case
ApUpdateRegular -> 0
ApUpdateAdd -> 1
ApUpdateInc -> 2
goOpcode :: Opcode -> Natural
goOpcode = \case
Nop -> 0
Call -> 1
Ret -> 2
AssertEq -> 4

View File

@ -1 +1,82 @@
module Juvix.Compiler.Backend.Cairo.Language where
module Juvix.Compiler.Backend.Cairo.Language
( module Juvix.Compiler.Backend.Cairo.Language,
module Juvix.Compiler.Casm.Language.Base,
module Juvix.Data.Field,
)
where
{-
This module defines data structures for the binary representation of Cairo
Assembly instructions, as defined in [1, Section 4]. See also:
https://github.com/lambdaclass/cairo-vm_in_go.
[1] Goldberg, Papini, Riabzev: "Cairo a Turing-complete STARK-friendly CPU
architecture" (https://ia.cr/2021/1063)
-}
import Juvix.Compiler.Casm.Language.Base
import Juvix.Data.Field
data Element
= ElementInstruction Instruction
| ElementImmediate FField
data Instruction = Instruction
{ _instrOffDst :: Offset,
_instrOffOp0 :: Offset,
_instrOffOp1 :: Offset,
_instrDstReg :: Reg,
_instrOp0Reg :: Reg,
_instrOp1Src :: Op1Src,
_instrResLogic :: ResLogic,
_instrPcUpdate :: PcUpdate,
_instrApUpdate :: ApUpdate,
_instrOpcode :: Opcode
}
data Op1Src
= Op1SrcOp0
| Op1SrcImm
| Op1SrcFp
| Op1SrcAp
data ResLogic
= ResOp1
| ResAdd
| ResMul
data PcUpdate
= PcUpdateRegular
| PcUpdateJump
| PcUpdateJumpRel
| PcUpdateJnz
data ApUpdate
= ApUpdateRegular
| ApUpdateAdd
| ApUpdateInc
data Opcode
= Nop
| Call
| Ret
| AssertEq
defaultInstruction :: Instruction
defaultInstruction =
Instruction
{ _instrOffDst = -1,
_instrOffOp0 = -1,
_instrOffOp1 = -1,
_instrDstReg = Ap,
_instrOp0Reg = Ap,
_instrOp1Src = Op1SrcAp,
_instrResLogic = ResOp1,
_instrPcUpdate = PcUpdateRegular,
_instrApUpdate = ApUpdateRegular,
_instrOpcode = Nop
}
makeLenses ''Instruction

View File

@ -1 +1,230 @@
module Juvix.Compiler.Backend.Cairo.Translation.FromCasm where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Backend.Cairo.Language
import Juvix.Compiler.Casm.Data.LabelInfo qualified as Casm
import Juvix.Compiler.Casm.Extra.LabelInfo qualified as Casm
import Juvix.Compiler.Casm.Language qualified as Casm
fromCasm :: [Casm.Instruction] -> [Element]
fromCasm instrs0 =
reverse $ snd $ foldl' (goInstr' (Casm.computeLabelInfo' instrSize instrs0)) (0, []) instrs0
where
unsupported :: Text -> a
unsupported msg = error ("Cairo: unsupported: " <> msg)
labelSyms =
mapMaybe
( \case
Casm.Label (Casm.LabelRef sym _) -> Just sym
_ -> Nothing
)
instrs0
instrSize :: Casm.Instruction -> Int
instrSize = length . goInstr dummyLabInfo 0
where
-- This LabelInfo has incorrect offsets -- it is used only to implement
-- `instrSize` needed to compute the correct LabelInfo
dummyLabInfo = Casm.LabelInfo $ HashMap.fromList $ zip labelSyms (repeat 0)
goInstr' :: Casm.LabelInfo -> (Address, [Element]) -> Casm.Instruction -> (Address, [Element])
goInstr' labInfo (addr, acc) i = (addr + length is, reverse is ++ acc)
where
is = goInstr labInfo addr i
goInstr :: Casm.LabelInfo -> Address -> Casm.Instruction -> [Element]
goInstr labInfo addr = \case
Casm.Assign x -> goAssign x
Casm.ExtraBinop x -> goExtraBinop x
Casm.Jump x -> goJump x
Casm.JumpIf x -> goJumpIf x
Casm.Call x -> goCall x
Casm.Return -> goReturn
Casm.Alloc x -> goAlloc x
Casm.Trace {} -> []
Casm.Label {} -> []
Casm.Nop -> []
where
updateDst :: Casm.MemRef -> Instruction -> Instruction
updateDst Casm.MemRef {..} instr =
instr
{ _instrOffDst = _memRefOff,
_instrDstReg = _memRefReg
}
updateOp0 :: Casm.MemRef -> Instruction -> Instruction
updateOp0 Casm.MemRef {..} instr =
instr
{ _instrOffOp0 = _memRefOff,
_instrOp0Reg = _memRefReg
}
updateOp1 :: Bool -> Casm.Value -> Instruction -> (Instruction, Maybe FField)
updateOp1 isRel v instr = case v of
Casm.Imm x ->
(instr', Just (fieldFromInteger cairoFieldSize x))
where
instr' =
instr
{ _instrOp1Src = Op1SrcImm,
_instrOffOp1 = 1
}
Casm.Ref Casm.MemRef {..} ->
(instr', Nothing)
where
src = case _memRefReg of
Ap -> Op1SrcAp
Fp -> Op1SrcFp
instr' =
instr
{ _instrOp1Src = src,
_instrOffOp1 = _memRefOff
}
Casm.Lab (Casm.LabelRef sym _) ->
(instr', Just (fieldFromInteger cairoFieldSize (fromIntegral labAddr)))
where
labValue = fromJust $ HashMap.lookup sym (labInfo ^. Casm.labelInfoTable)
labAddr :: Address
labAddr
| isRel = labValue - addr
| otherwise = labValue
instr' =
instr
{ _instrOp1Src = Op1SrcImm,
_instrOffOp1 = 1
}
updateOps :: Bool -> Casm.RValue -> Instruction -> (Instruction, Maybe FField)
updateOps isRel rv instr = case rv of
Casm.Val v ->
updateOp1 isRel v instr
Casm.Load Casm.LoadValue {..} ->
(instr'', Nothing)
where
instr' = updateOp0 _loadValueSrc instr
instr'' =
instr'
{ _instrOp1Src = Op1SrcOp0,
_instrOffOp1 = _loadValueOff
}
Casm.Binop Casm.BinopValue {..} ->
(instr'', mf)
where
(instr', mf) = updateOp1 isRel _binopValueArg2 (updateOp0 _binopValueArg1 instr)
instr'' =
instr'
{ _instrResLogic = case _binopValueOpcode of
Casm.FieldAdd -> ResAdd
Casm.FieldMul -> ResMul
}
updateIncAp :: Bool -> Instruction -> Instruction
updateIncAp incAp instr =
instr
{ _instrApUpdate = if incAp then ApUpdateInc else ApUpdateRegular
}
toElems :: (Instruction, Maybe FField) -> [Element]
toElems (instr, mf) =
ElementInstruction instr : maybeToList (fmap ElementImmediate mf)
goAssign :: Casm.InstrAssign -> [Element]
goAssign Casm.InstrAssign {..} =
toElems
. updateOps False _instrAssignValue
. updateDst _instrAssignResult
. updateIncAp _instrAssignIncAp
. set instrOpcode AssertEq
$ defaultInstruction
goBinop :: Bool -> Casm.Opcode -> Casm.MemRef -> Casm.MemRef -> Casm.Value -> [Element]
goBinop incAp op res arg1 arg2 =
toElems
. updateOps False (Casm.Binop $ Casm.BinopValue op arg1 arg2)
. updateDst res
. updateIncAp incAp
. set instrOpcode AssertEq
$ defaultInstruction
goExtraBinop :: Casm.InstrExtraBinop -> [Element]
goExtraBinop Casm.InstrExtraBinop {..} = case _instrExtraBinopOpcode of
Casm.FieldSub ->
goBinop _instrExtraBinopIncAp Casm.FieldAdd _instrExtraBinopArg1 _instrExtraBinopResult _instrExtraBinopArg2
Casm.FieldDiv ->
goBinop _instrExtraBinopIncAp Casm.FieldMul _instrExtraBinopArg1 _instrExtraBinopResult _instrExtraBinopArg2
Casm.IntAdd ->
-- TODO: range check
goBinop _instrExtraBinopIncAp Casm.FieldAdd _instrExtraBinopResult _instrExtraBinopArg1 _instrExtraBinopArg2
Casm.IntSub ->
-- TODO: range check
goBinop _instrExtraBinopIncAp Casm.FieldAdd _instrExtraBinopArg1 _instrExtraBinopResult _instrExtraBinopArg2
Casm.IntMul ->
-- TODO: range check
goBinop _instrExtraBinopIncAp Casm.FieldMul _instrExtraBinopResult _instrExtraBinopArg1 _instrExtraBinopArg2
Casm.IntDiv ->
unsupported "integer division"
Casm.IntMod ->
unsupported "integer modulus"
Casm.IntLt ->
unsupported "integer comparison"
goJump :: Casm.InstrJump -> [Element]
goJump Casm.InstrJump {..} =
toElems
. updateOps _instrJumpRel _instrJumpTarget
. updateIncAp _instrJumpIncAp
. set instrPcUpdate pcUpdate
$ defaultInstruction
where
pcUpdate = if _instrJumpRel then PcUpdateJumpRel else PcUpdateJump
goJumpIf :: Casm.InstrJumpIf -> [Element]
goJumpIf Casm.InstrJumpIf {..} =
toElems
. updateOp1 True _instrJumpIfTarget
. updateDst _instrJumpIfValue
. updateIncAp _instrJumpIfIncAp
. set instrPcUpdate PcUpdateJnz
$ defaultInstruction
goCall :: Casm.InstrCall -> [Element]
goCall Casm.InstrCall {..} =
toElems
. updateOp1 _instrCallRel _instrCallTarget
$ defaultInstruction
{ _instrOffDst = 0,
_instrDstReg = Ap,
_instrOffOp0 = 1,
_instrOp0Reg = Ap,
_instrPcUpdate = pcUpdate,
_instrOpcode = Call
}
where
pcUpdate = if _instrCallRel then PcUpdateJumpRel else PcUpdateJump
goReturn :: [Element]
goReturn =
[ ElementInstruction $
Instruction
{ _instrOffDst = -2,
_instrOffOp0 = -1,
_instrOffOp1 = -1,
_instrDstReg = Fp,
_instrOp0Reg = Fp,
_instrOp1Src = Op1SrcFp,
_instrResLogic = ResOp1,
_instrPcUpdate = PcUpdateJump,
_instrApUpdate = ApUpdateRegular,
_instrOpcode = Ret
}
]
goAlloc :: Casm.InstrAlloc -> [Element]
goAlloc Casm.InstrAlloc {..} =
toElems
. updateOps False _instrAllocSize
. set instrApUpdate ApUpdateAdd
$ defaultInstruction

View File

@ -91,17 +91,17 @@ mkOpArgsNum res v =
mkExtraBinop FieldSub res (MemRef Ap (-2)) (Ref $ MemRef Ap (-1))
]
mkCall :: Value -> Instruction
mkCall = Call . InstrCall
mkCallRel :: Value -> Instruction
mkCallRel tgt = Call (InstrCall tgt True)
mkJump :: RValue -> Instruction
mkJump tgt = Jump (InstrJump tgt False False)
mkCallAbs :: Value -> Instruction
mkCallAbs tgt = Call (InstrCall tgt False)
mkJumpAbs :: RValue -> Instruction
mkJumpAbs tgt = Jump (InstrJump tgt False False)
mkJumpIf :: Value -> MemRef -> Instruction
mkJumpIf tgt v = JumpIf (InstrJumpIf tgt v False False)
mkJumpIf tgt v = JumpIf (InstrJumpIf tgt v False)
mkJumpRel :: RValue -> Instruction
mkJumpRel tgt = Jump (InstrJump tgt True False)
mkJumpRelIf :: Value -> MemRef -> Instruction
mkJumpRelIf tgt v = JumpIf (InstrJumpIf tgt v True False)

View File

@ -0,0 +1,20 @@
module Juvix.Compiler.Casm.Extra.LabelInfo where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Casm.Data.LabelInfo
import Juvix.Compiler.Casm.Language
computeLabelInfo' :: (Instruction -> Int) -> [Instruction] -> LabelInfo
computeLabelInfo' sizeFun = go 0 mempty
where
go :: Address -> LabelInfo -> [Instruction] -> LabelInfo
go addr acc = \case
[] ->
acc
i@(Label (LabelRef sym _)) : instrs' ->
go (addr + sizeFun i) (over labelInfoTable (HashMap.insert sym addr) acc) instrs'
i : instrs' ->
go (addr + sizeFun i) acc instrs'
computeLabelInfo :: [Instruction] -> LabelInfo
computeLabelInfo = computeLabelInfo' (const 1)

View File

@ -47,13 +47,10 @@ hRunCode hout (LabelInfo labelInfo) instrs0 = runST goCode
Memory s ->
ST s FField
go pc ap fp mem
| Vec.length instrs <= pc = do
when (Vec.length instrs < pc) $
throwRunError ("invalid program counter: " <> show pc)
checkGaps mem
when (ap == 0) $
throwRunError "nothing to return"
readMem mem (ap - 1)
| Vec.length instrs == pc =
goFinish ap mem
| Vec.length instrs < pc =
throwRunError ("invalid program counter: " <> show pc)
| otherwise =
case instrs Vec.! pc of
Assign x -> goAssign x pc ap fp mem
@ -65,6 +62,7 @@ hRunCode hout (LabelInfo labelInfo) instrs0 = runST goCode
Alloc x -> goAlloc x pc ap fp mem
Trace x -> goTrace x pc ap fp mem
Label {} -> go (pc + 1) ap fp mem
Nop -> go (pc + 1) ap fp mem
checkGaps :: forall s. Memory s -> ST s ()
checkGaps mem = goGaps False 0
@ -131,11 +129,16 @@ hRunCode hout (LabelInfo labelInfo) instrs0 = runST goCode
fromMaybe (throwRunError "invalid label") $
HashMap.lookup _labelRefSymbol labelInfo
readValue :: Address -> Address -> Memory s -> Value -> ST s FField
readValue ap fp mem = \case
readValue' :: Bool -> Address -> Address -> Address -> Memory s -> Value -> ST s FField
readValue' isRel pc ap fp mem = \case
Imm v -> return $ fieldFromInteger fsize v
Ref r -> readMemRef ap fp mem r
Lab l -> return $ readLabel l
Lab l -> return $ if isRel then fieldSub lab (fieldFromInteger fsize (fromIntegral pc)) else lab
where
lab = readLabel l
readValue :: Address -> Address -> Memory s -> Value -> ST s FField
readValue = readValue' False 0
readLoadValue :: Address -> Address -> Memory s -> LoadValue -> ST s FField
readLoadValue ap fp mem LoadValue {..} = do
@ -155,12 +158,15 @@ hRunCode hout (LabelInfo labelInfo) instrs0 = runST goCode
FieldAdd -> fieldAdd x y
FieldMul -> fieldMul x y
readRValue :: Address -> Address -> Memory s -> RValue -> ST s FField
readRValue ap fp mem = \case
Val x -> readValue ap fp mem x
readRValue' :: Bool -> Address -> Address -> Address -> Memory s -> RValue -> ST s FField
readRValue' isRel pc ap fp mem = \case
Val x -> readValue' isRel pc ap fp mem x
Load x -> readLoadValue ap fp mem x
Binop x -> readBinopValue ap fp mem x
readRValue :: Address -> Address -> Memory s -> RValue -> ST s FField
readRValue = readRValue' False 0
goAssign :: InstrAssign -> Address -> Address -> Address -> Memory s -> ST s FField
goAssign InstrAssign {..} pc ap fp mem = do
v <- readRValue ap fp mem _instrAssignValue
@ -197,29 +203,32 @@ hRunCode hout (LabelInfo labelInfo) instrs0 = runST goCode
goJump :: InstrJump -> Address -> Address -> Address -> Memory s -> ST s FField
goJump InstrJump {..} pc ap fp mem = do
tgt <- readRValue ap fp mem _instrJumpTarget
tgt <- readRValue' _instrJumpRel pc ap fp mem _instrJumpTarget
let off = if _instrJumpRel then pc else 0
go (off + fromInteger (fieldToInteger tgt)) (ap + fromEnum _instrJumpIncAp) fp mem
goJumpIf :: InstrJumpIf -> Address -> Address -> Address -> Memory s -> ST s FField
goJumpIf InstrJumpIf {..} pc ap fp mem = do
tgt <- readValue ap fp mem _instrJumpIfTarget
tgt <- readValue' True pc ap fp mem _instrJumpIfTarget
v <- readMemRef ap fp mem _instrJumpIfValue
let off = if _instrJumpIfRel then pc else 0
go (if fieldToInteger v /= 0 then off + fromInteger (fieldToInteger tgt) else pc + 1) (ap + fromEnum _instrJumpIfIncAp) fp mem
go (if fieldToInteger v /= 0 then pc + fromInteger (fieldToInteger tgt) else pc + 1) (ap + fromEnum _instrJumpIfIncAp) fp mem
goCall :: InstrCall -> Address -> Address -> Address -> Memory s -> ST s FField
goCall InstrCall {..} pc ap fp mem = do
tgt <- readValue ap fp mem _instrCallTarget
tgt <- readValue' _instrCallRel pc ap fp mem _instrCallTarget
mem' <- writeMem mem ap (fieldFromInteger fsize (fromIntegral fp))
mem'' <- writeMem mem' (ap + 1) (fieldFromInteger fsize (fromIntegral pc + 1))
go (fromInteger (fieldToInteger tgt)) (ap + 2) (ap + 2) mem''
let off = if _instrCallRel then pc else 0
go (off + fromInteger (fieldToInteger tgt)) (ap + 2) (ap + 2) mem''
goReturn :: Address -> Address -> Address -> Memory s -> ST s FField
goReturn _ ap fp mem = do
pc' <- readMem mem (fp - 1)
fp' <- readMem mem (fp - 2)
go (fromInteger (fieldToInteger pc')) ap (fromInteger (fieldToInteger fp')) mem
goReturn _ ap fp mem
| fp == 0 =
goFinish ap mem
| otherwise = do
pc' <- readMem mem (fp - 1)
fp' <- readMem mem (fp - 2)
go (fromInteger (fieldToInteger pc')) ap (fromInteger (fieldToInteger fp')) mem
goAlloc :: InstrAlloc -> Address -> Address -> Address -> Memory s -> ST s FField
goAlloc InstrAlloc {..} pc ap fp mem = do
@ -232,6 +241,13 @@ hRunCode hout (LabelInfo labelInfo) instrs0 = runST goCode
GHC.unsafePerformIO (hPrint hout v >> return (pure ()))
go (pc + 1) ap fp mem
goFinish :: Address -> Memory s -> ST s FField
goFinish ap mem = do
checkGaps mem
when (ap == 0) $
throwRunError "nothing to return"
readMem mem (ap - 1)
catchRunErrorIO :: a -> IO (Either CasmError a)
catchRunErrorIO a =
Exception.catch

View File

@ -8,6 +8,7 @@ where
import Juvix.Data.Keyword
import Juvix.Data.Keyword.All
( delimSemicolon,
kwAbs,
kwAp,
kwApPlusPlus,
kwCall,
@ -25,6 +26,7 @@ import Juvix.Data.Keyword.All
kwJmp,
kwMinus,
kwMul,
kwNop,
kwNotEq,
kwPlus,
kwPlusEq,
@ -40,6 +42,7 @@ allKeywordStrings = keywordsStrings allKeywords
allKeywords :: [Keyword]
allKeywords =
[ delimSemicolon,
kwAbs,
kwAp,
kwApPlusPlus,
kwCall,
@ -57,6 +60,7 @@ allKeywords =
kwJmp,
kwMinus,
kwMul,
kwNop,
kwNotEq,
kwPlus,
kwPlusEq,

View File

@ -20,14 +20,6 @@ follow the syntax of [1, Section 5].
import Juvix.Compiler.Casm.Language.Base
type Offset = Int16
type Address = Int
data Reg
= Ap
| Fp
data MemRef = MemRef
{ _memRefReg :: Reg,
_memRefOff :: Offset
@ -94,6 +86,7 @@ data Instruction
| Alloc InstrAlloc
| Trace InstrTrace
| Label LabelRef
| Nop
data InstrAssign = InstrAssign
{ _instrAssignValue :: RValue,
@ -120,12 +113,12 @@ data InstrJump = InstrJump
data InstrJumpIf = InstrJumpIf
{ _instrJumpIfTarget :: Value,
_instrJumpIfValue :: MemRef,
_instrJumpIfRel :: Bool,
_instrJumpIfIncAp :: Bool
}
newtype InstrCall = InstrCall
{ _instrCallTarget :: Value
data InstrCall = InstrCall
{ _instrCallTarget :: Value,
_instrCallRel :: Bool
}
newtype InstrAlloc = InstrAlloc

View File

@ -1,6 +1,15 @@
module Juvix.Compiler.Casm.Language.Base
( module Juvix.Compiler.Core.Language.Base,
module Juvix.Compiler.Casm.Language.Base,
)
where
import Juvix.Compiler.Core.Language.Base hiding (Ap, Index)
type Offset = Int16
type Address = Int
data Reg
= Ap
| Fp

View File

@ -112,11 +112,22 @@ instance PrettyCode InstrExtraBinop where
incAp <- ppIncAp _instrExtraBinopIncAp
return $ r <+> Str.equal <+> v1 <+> op <+> v2 <> incAp
ppRel :: Bool -> RValue -> Sem r (Doc Ann)
ppRel isRel tgt
| isLab tgt = return mempty
| isRel = return $ Str.rel <> space
| otherwise = return $ Str.abs <> space
where
isLab :: RValue -> Bool
isLab = \case
Val Lab {} -> True
_ -> False
instance PrettyCode InstrJump where
ppCode InstrJump {..} = do
tgt <- ppCode _instrJumpTarget
incAp <- ppIncAp _instrJumpIncAp
let rel = if _instrJumpRel then Str.rel <> space else mempty
rel <- ppRel _instrJumpRel _instrJumpTarget
return $ Str.jmp <+> rel <> tgt <> incAp
instance PrettyCode InstrJumpIf where
@ -124,13 +135,13 @@ instance PrettyCode InstrJumpIf where
tgt <- ppCode _instrJumpIfTarget
v <- ppCode _instrJumpIfValue
incAp <- ppIncAp _instrJumpIfIncAp
let rel = if _instrJumpIfRel then Str.rel <> space else mempty
return $ Str.jmp <+> rel <> tgt <+> Str.if_ <+> v <+> Str.notequal <+> annotate AnnLiteralInteger "0" <> incAp
return $ Str.jmp <+> tgt <+> Str.if_ <+> v <+> Str.notequal <+> annotate AnnLiteralInteger "0" <> incAp
instance PrettyCode InstrCall where
ppCode InstrCall {..} = do
tgt <- ppCode _instrCallTarget
return $ Str.call <+> tgt
rel <- ppRel _instrCallRel (Val _instrCallTarget)
return $ Str.call <+> rel <> tgt
instance PrettyCode InstrAlloc where
ppCode InstrAlloc {..} = do
@ -153,3 +164,4 @@ instance PrettyCode Instruction where
Alloc x -> ppCode x
Trace x -> ppCode x
Label x -> (<> colon) <$> ppCode x
Nop -> return Str.nop

View File

@ -19,25 +19,33 @@ fromReg :: Reg.InfoTable -> Result
fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolId tab) $ do
let initialOffset :: Int = 2
(blts, binstrs) <- addStdlibBuiltins initialOffset
let cinstrs = concatMap (mkFunCall . fst) $ sortOn snd $ HashMap.toList (info ^. Reg.extraInfoFUIDs)
endSym <- freshSymbol
let endName :: Text = "__juvix_end"
endLab = LabelRef endSym (Just endName)
(addr, instrs) <- second (concat . reverse) <$> foldM (goFun blts endLab) (initialOffset + length binstrs, []) (tab ^. Reg.infoFunctions)
eassert (addr == length instrs + length binstrs + initialOffset)
(addr, instrs) <- second (concat . reverse) <$> foldM (goFun blts endLab) (initialOffset + length binstrs + length cinstrs, []) (tab ^. Reg.infoFunctions)
eassert (addr == length instrs + length cinstrs + length binstrs + initialOffset)
registerLabelName endSym endName
registerLabelAddress endSym addr
let mainSym = fromJust $ tab ^. Reg.infoMainFunction
mainName = fromJust (HashMap.lookup mainSym (tab ^. Reg.infoFunctions)) ^. Reg.functionName
callInstr = Call $ InstrCall $ Lab $ LabelRef mainSym (Just mainName)
jmpInstr = mkJump (Val $ Lab endLab)
return $ callInstr : jmpInstr : binstrs ++ instrs ++ [Label endLab]
callInstr = mkCallRel (Lab $ LabelRef mainSym (Just mainName))
jmpInstr = mkJumpRel (Val $ Lab endLab)
return $ callInstr : jmpInstr : binstrs ++ cinstrs ++ instrs ++ [Label endLab]
where
info :: Reg.ExtraInfo
info = Reg.computeExtraInfo (getLimits TargetCairo False) tab
mkFunCall :: Symbol -> [Instruction]
mkFunCall sym =
[ mkCallRel $ Lab $ LabelRef sym (Just $ Reg.lookupFunInfo tab sym ^. Reg.functionName),
Return,
Nop
]
getTagId :: Tag -> Int
getTagId tag =
1 + fromJust (HashMap.lookup tag (info ^. Reg.extraInfoCIDs))
1 + 2 * fromJust (HashMap.lookup tag (info ^. Reg.extraInfoCIDs))
goFun :: forall r. (Member LabelInfoBuilder r) => StdlibBuiltins -> LabelRef -> (Address, [[Instruction]]) -> Reg.FunctionInfo -> Sem r (Address, [[Instruction]])
goFun blts failLab (addr0, acc) funInfo = do
@ -212,7 +220,7 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
mkAllocCall :: MemRef -> [Instruction]
mkAllocCall res =
[ mkCall $ Lab $ LabelRef (blts ^. stdlibGetRegs) (Just (blts ^. stdlibGetRegsName)),
[ mkCallRel $ Lab $ LabelRef (blts ^. stdlibGetRegs) (Just (blts ^. stdlibGetRegsName)),
mkNativeBinop FieldAdd res (MemRef Ap (-2)) (Imm 2)
]
@ -231,14 +239,14 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
goAllocClosure _ Reg.InstrAllocClosure {..} =
return $
mkAllocCall res
++ [ mkAssignAp (Val $ Lab $ LabelRef _instrAllocClosureSymbol (Just funName)),
++ [ mkAssignAp (Val $ Imm $ fromIntegral $ 1 + 3 * fuid),
mkAssignAp (Val $ Imm $ fromIntegral $ casmMaxFunctionArgs + 1 - storedArgsNum),
mkAssignAp (Val $ Imm $ fromIntegral $ casmMaxFunctionArgs + 1 - leftArgsNum)
]
++ map goAssignApValue _instrAllocClosureArgs
where
res = goVarRef _instrAllocClosureResult
funName = Reg.lookupFunInfo tab _instrAllocClosureSymbol ^. Reg.functionName
fuid = fromJust $ HashMap.lookup _instrAllocClosureSymbol (info ^. Reg.extraInfoFUIDs)
storedArgsNum = length _instrAllocClosureArgs
leftArgsNum = _instrAllocClosureExpectedArgsNum - storedArgsNum
@ -248,7 +256,7 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
map goAssignApValue _instrExtendClosureArgs
++ [ mkAssignAp (Val $ Imm $ fromIntegral $ length _instrExtendClosureArgs),
mkAssignAp (Val $ Ref val),
mkCall $ Lab $ LabelRef (blts ^. stdlibExtendClosure) (Just (blts ^. stdlibExtendClosureName)),
mkCallRel $ Lab $ LabelRef (blts ^. stdlibExtendClosure) (Just (blts ^. stdlibExtendClosureName)),
mkAssign res (Val $ Ref $ MemRef Ap (-1))
]
where
@ -259,7 +267,7 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
goCall' saveOrRet ct args = case ct of
Reg.CallFun sym ->
args'
++ [ mkCall $ Lab $ LabelRef sym (Just funName),
++ [ mkCallRel $ Lab $ LabelRef sym (Just funName),
saveOrRet
]
where
@ -267,7 +275,7 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
Reg.CallClosure cl ->
args'
++ [ mkAssignAp (Val $ Ref $ goVarRef cl),
mkCall $ Lab $ LabelRef (blts ^. stdlibCallClosure) (Just (blts ^. stdlibCallClosureName)),
mkCallRel $ Lab $ LabelRef (blts ^. stdlibCallClosure) (Just (blts ^. stdlibCallClosureName)),
saveOrRet
]
where
@ -315,7 +323,7 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
is
++ [mkJumpIf (Lab labFalse) r]
++ codeTrue
++ [ mkJump (Val $ Lab labEnd),
++ [ mkJumpRel (Val $ Lab labEnd),
Label labFalse
]
++ codeFalse
@ -331,14 +339,18 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
let symMap = HashMap.fromList $ zip tags syms
labs = map (flip LabelRef Nothing) syms
labEnd = LabelRef symEnd Nothing
jmps = map (mkJump . Val . Lab) labs
addr1 = addr + length is + 1 + length jmps
jmps = map (mkJumpRel . Val . Lab) labs
-- we need the Nop instructions to ensure that the relative jump
-- offsets in our CASM interpreter correspond to the relative jump
-- offsets in the Cairo binary representation
jmps' = concatMap (\i -> [i, Nop]) jmps
addr1 = addr + length is + 1 + length jmps'
(addr2, instrs) <- second (concat . reverse) <$> foldM (goCaseBranch symMap labEnd) (addr1, []) _instrCaseBranches
(addr3, instrs') <- second reverse <$> foldM (goDefaultLabel symMap) (addr2, []) defaultTags
instrs'' <- maybe (return []) (goCode addr3) _instrCaseDefault
let addr4 = addr3 + length instrs''
registerLabelAddress symEnd addr4
return $ is ++ mkJumpRel v : jmps ++ instrs ++ instrs' ++ instrs'' ++ [Label labEnd]
return $ is ++ mkJumpRel v : jmps' ++ instrs ++ instrs' ++ instrs'' ++ [Label labEnd]
where
(is, v) = goLoad _instrCaseValue 0
tags = Reg.lookupInductiveInfo tab _instrCaseInductive ^. Reg.inductiveConstructors
@ -351,7 +363,7 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
lab = LabelRef sym Nothing
registerLabelAddress sym addr'
instrs <- goCode (addr' + 1) _caseBranchCode
let instrs' = Label lab : instrs ++ [mkJump (Val $ Lab labEnd)]
let instrs' = Label lab : instrs ++ [mkJumpRel (Val $ Lab labEnd)]
return (addr' + length instrs', instrs' : acc')
goDefaultLabel :: HashMap Tag Symbol -> (Address, [Instruction]) -> Reg.Tag -> Sem r (Address, [Instruction])
@ -369,7 +381,7 @@ fromReg tab = uncurry Result $ run $ runLabelInfoBuilderWithNextId (Reg.getNextS
goFail _ Reg.InstrFailure {..} =
return
[ Trace (InstrTrace (goRValue _instrFailureValue)),
mkJump (Val $ Lab failLab)
mkJumpRel (Val $ Lab failLab)
]
goBlock :: Address -> Reg.InstrBlock -> Sem r [Instruction]

View File

@ -68,7 +68,12 @@ label addr = P.try $ do
instruction :: (Member LabelInfoBuilder r) => ParsecS r Instruction
instruction =
parseAlloc <|> parseJump <|> parseCall <|> parseReturn <|> parseTrace <|> parseAssign
parseNop <|> parseAlloc <|> parseJump <|> parseCall <|> parseReturn <|> parseTrace <|> parseAssign
parseNop :: ParsecS r Instruction
parseNop = do
kw kwNop
return Nop
parseAlloc :: (Member LabelInfoBuilder r) => ParsecS r Instruction
parseAlloc = do
@ -164,6 +169,9 @@ parseLabel = do
parseIncAp :: ParsecS r Bool
parseIncAp = (kw delimSemicolon >> kw kwApPlusPlus >> return True) <|> return False
parseRel :: ParsecS r Bool
parseRel = (kw kwRel >> return True) <|> (kw kwAbs >> return False) <|> return True
parseJump :: forall r. (Member LabelInfoBuilder r) => ParsecS r Instruction
parseJump = do
kw kwJmp
@ -171,7 +179,6 @@ parseJump = do
where
jmpIf :: ParsecS r Instruction
jmpIf = do
isRel <- isJust <$> optional (kw kwRel)
tgt <- parseValue
kw kwIf
v <- parseMemRef
@ -183,13 +190,12 @@ parseJump = do
InstrJumpIf
{ _instrJumpIfTarget = tgt,
_instrJumpIfValue = v,
_instrJumpIfRel = isRel,
_instrJumpIfIncAp = incAp
}
jmp :: ParsecS r Instruction
jmp = do
isRel <- isJust <$> optional (kw kwRel)
isRel <- parseRel
tgt <- parseRValue
incAp <- parseIncAp
return $
@ -203,8 +209,9 @@ parseJump = do
parseCall :: (Member LabelInfoBuilder r) => ParsecS r Instruction
parseCall = do
kw kwCall
isRel <- parseRel
v <- parseValue
return $ Call $ InstrCall {_instrCallTarget = v}
return $ Call $ InstrCall {_instrCallTarget = v, _instrCallRel = isRel}
parseReturn :: ParsecS r Instruction
parseReturn = do

View File

@ -20,6 +20,7 @@ validate labi instrs = mapM_ go instrs
Alloc x -> goAlloc x
Trace x -> goTrace x
Label {} -> return ()
Nop -> return ()
goLabelRef :: LabelRef -> Either CasmError ()
goLabelRef l@LabelRef {..} = do

View File

@ -14,6 +14,7 @@ import Juvix.Compiler.Asm.Pipeline qualified as Asm
import Juvix.Compiler.Asm.Translation.FromTree qualified as Asm
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.C qualified as C
import Juvix.Compiler.Backend.Cairo qualified as Cairo
import Juvix.Compiler.Backend.Geb qualified as Geb
import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR
import Juvix.Compiler.Casm.Data.Result qualified as Casm
@ -109,6 +110,12 @@ upToCasm ::
upToCasm =
upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToCasm _coreResultModule
upToCairo ::
(Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
Sem r Cairo.Result
upToCairo =
upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToCairo _coreResultModule
upToMiniC ::
(Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, GitClone, PathResolver] r) =>
Sem r C.MiniCResult
@ -164,6 +171,9 @@ storedCoreToMiniC = storedCoreToAsm >=> asmToMiniC
storedCoreToCasm :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Casm.Result
storedCoreToCasm = local (set entryPointFieldSize cairoFieldSize) . storedCoreToTree Core.CheckCairo >=> treeToCasm
storedCoreToCairo :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Cairo.Result
storedCoreToCairo = storedCoreToCasm >=> casmToCairo
storedCoreToGeb :: (Members '[Error JuvixError, Reader EntryPoint] r) => Geb.ResultSpec -> Core.Module -> Sem r Geb.Result
storedCoreToGeb spec = Core.toGeb >=> return . uncurry (Geb.toResult spec) . Geb.fromCore . Core.computeCombinedInfoTable
@ -189,6 +199,9 @@ coreToReg = Core.toStored >=> storedCoreToReg
coreToCasm :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Casm.Result
coreToCasm = Core.toStored >=> storedCoreToCasm
coreToCairo :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Cairo.Result
coreToCairo = Core.toStored >=> storedCoreToCairo
coreToAnoma :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r NockmaTree.AnomaResult
coreToAnoma = coreToTree Core.CheckAnoma >=> treeToAnoma
@ -226,12 +239,18 @@ treeToMiniC = treeToAsm >=> asmToMiniC
treeToCasm :: (Members '[Error JuvixError, Reader EntryPoint] r) => Tree.InfoTable -> Sem r Casm.Result
treeToCasm = treeToCairoAsm >=> asmToCasm
treeToCairo :: (Members '[Error JuvixError, Reader EntryPoint] r) => Tree.InfoTable -> Sem r Cairo.Result
treeToCairo = treeToCasm >=> casmToCairo
asmToReg :: (Members '[Error JuvixError, Reader EntryPoint] r) => Asm.InfoTable -> Sem r Reg.InfoTable
asmToReg = Asm.toReg >=> return . Reg.fromAsm
asmToCasm :: (Members '[Error JuvixError, Reader EntryPoint] r) => Asm.InfoTable -> Sem r Casm.Result
asmToCasm = asmToReg >=> regToCasm
asmToCairo :: (Members '[Error JuvixError, Reader EntryPoint] r) => Asm.InfoTable -> Sem r Cairo.Result
asmToCairo = asmToReg >=> regToCairo
asmToMiniC :: (Members '[Error JuvixError, Reader EntryPoint] r) => Asm.InfoTable -> Sem r C.MiniCResult
asmToMiniC = asmToReg >=> regToMiniC
@ -244,6 +263,12 @@ regToMiniC tab = do
regToCasm :: Reg.InfoTable -> Sem r Casm.Result
regToCasm = Reg.toCasm >=> return . Casm.fromReg
casmToCairo :: Casm.Result -> Sem r Cairo.Result
casmToCairo Casm.Result {..} = return $ Cairo.serialize $ Cairo.fromCasm _resultCode
regToCairo :: Reg.InfoTable -> Sem r Cairo.Result
regToCairo = regToCasm >=> casmToCairo
treeToAnoma' :: (Members '[Error JuvixError, Reader NockmaTree.CompilerOptions] r) => Tree.InfoTable -> Sem r NockmaTree.AnomaResult
treeToAnoma' = Tree.toNockma >=> NockmaTree.fromTreeTable

View File

@ -90,6 +90,11 @@ fieldToInteger
(FField ((_ :: Sing (p :: Natural)) :&: (f1 :: PrimeField p))) =
toInteger f1
fieldToNatural :: FField -> Natural
fieldToNatural f = (fromIntegral (fieldToInteger f) + s) `mod` s
where
s = fieldSize f
fieldResize :: Natural -> FField -> FField
fieldResize n f = fieldFromInteger n (fieldToInteger f)

View File

@ -16,6 +16,7 @@ data FileExt
| FileExtJuvixReg
| FileExtJuvixTree
| FileExtCasm
| FileExtJson
| FileExtVampIR
| FileExtVampIRParams
| FileExtPlonk
@ -52,6 +53,9 @@ juvixTreeFileExt = ".jvt"
casmFileExt :: (IsString a) => a
casmFileExt = ".casm"
jsonFileExt :: (IsString a) => a
jsonFileExt = ".json"
vampIRFileExt :: (IsString a) => a
vampIRFileExt = ".pir"
@ -92,6 +96,7 @@ fileExtToText = \case
FileExtJuvixReg -> juvixRegFileExt
FileExtJuvixTree -> juvixTreeFileExt
FileExtCasm -> casmFileExt
FileExtJson -> jsonFileExt
FileExtVampIR -> vampIRFileExt
FileExtVampIRParams -> vampIRParamsFileExt
FileExtPlonk -> plonkFileExt
@ -113,6 +118,7 @@ toMetavar = \case
FileExtJuvixReg -> "JUVIX_REG_FILE"
FileExtJuvixTree -> "JUVIX_TREE_FILE"
FileExtCasm -> "CASM_FILE"
FileExtJson -> "JSON_FILE"
FileExtVampIR -> "VAMPIR_FILE"
FileExtVampIRParams -> "VAMPIR_PARAMS_FILE"
FileExtPlonk -> "PLONK_FILE"

View File

@ -1,8 +1,8 @@
module Casm.Compilation.Base where
import Base
import Casm.Run.Base
import Juvix.Compiler.Casm.Data.Result
import Juvix.Compiler.Casm.Interpreter
import Juvix.Compiler.Casm.Pretty
import Juvix.Compiler.Core qualified as Core
import Juvix.Data.Field
@ -36,17 +36,8 @@ compileAssertionEntry adjustEntry root' optLevel mainFile expectedFile step = do
Right Result {..} -> do
withTempDir'
( \dirPath -> do
let outputFile = dirPath <//> $(mkRelFile "out.out")
let tmpFile = dirPath <//> $(mkRelFile "tmp.out")
step "Serialize"
writeFileEnsureLn tmpFile (toPlainText $ ppProgram _resultCode)
hout <- openFile (toFilePath outputFile) WriteMode
step "Interpret"
let v = hRunCode hout _resultLabelInfo _resultCode
hPutStrLn hout (show v)
hClose hout
actualOutput <- readFile outputFile
step "Compare expected and actual program output"
expected <- readFile expectedFile
assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
)
casmRunAssertion' False _resultLabelInfo _resultCode expectedFile step

View File

@ -1,7 +1,8 @@
module Casm.Reg where
import Base
-- import Casm.Reg.Cairo qualified as C
import Casm.Reg.Positive qualified as P
allTests :: TestTree
allTests = testGroup "CASM from JuvixReg translation" [P.allTests]
allTests = testGroup "JuvixReg to CASM translation" [P.allTests]

View File

@ -1,20 +1,41 @@
module Casm.Reg.Base where
import Base
import Casm.Run.Base qualified as Run
import Data.Aeson
import Juvix.Compiler.Casm.Data.Result
import Juvix.Compiler.Casm.Interpreter
import Juvix.Compiler.Reg.Data.InfoTable qualified as Reg
import Juvix.Data.PPOutput
import Reg.Run.Base qualified as Reg
compileAssertion' :: Handle -> Symbol -> Reg.InfoTable -> IO ()
compileAssertion' hout _ tab = do
compileAssertion' :: Path Abs Dir -> Path Abs File -> Symbol -> Reg.InfoTable -> (String -> IO ()) -> Assertion
compileAssertion' _ outputFile _ tab step = do
step "Translate to CASM"
case run $ runError @JuvixError $ regToCasm tab of
Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
Right Result {..} -> do
hout <- openFile (toFilePath outputFile) WriteMode
let v = hRunCode hout _resultLabelInfo _resultCode
hPutStrLn hout (show v)
hPrint hout v
hClose hout
cairoAssertion' :: Path Abs Dir -> Path Abs File -> Symbol -> Reg.InfoTable -> (String -> IO ()) -> Assertion
cairoAssertion' dirPath outputFile _ tab step = do
step "Translate to Cairo"
case run $ runError @JuvixError $ regToCairo tab of
Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
Right res -> do
step "Serialize to Cairo bytecode"
encodeFile (toFilePath outputFile) res
step "Execute in Cairo VM"
actualOutput <- Run.casmRunVM' dirPath outputFile
writeFileEnsureLn outputFile actualOutput
regToCasmAssertion :: Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion
regToCasmAssertion mainFile expectedFile step =
Reg.regRunAssertionParam compileAssertion' mainFile expectedFile [] (const (return ())) step
regToCairoAssertion :: Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion
regToCairoAssertion mainFile expectedFile step =
Reg.regRunAssertionParam cairoAssertion' mainFile expectedFile [] (const (return ())) step

26
test/Casm/Reg/Cairo.hs Normal file
View File

@ -0,0 +1,26 @@
module Casm.Reg.Cairo where
import Base
import Casm.Reg.Base
import Casm.Reg.Positive qualified as P
testDescr :: P.PosTest -> TestDescr
testDescr P.PosTest {..} =
let tRoot = P.root <//> _relDir
file' = tRoot <//> _file
expected' = tRoot <//> _expectedFile
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Steps $ regToCairoAssertion file' expected'
}
allTests :: TestTree
allTests =
testGroup
"JuvixReg to Cairo translation positive tests"
( map (mkTest . testDescr) $
P.filterOutTests
[]
P.tests
)

View File

@ -24,13 +24,13 @@ testDescr PosTest {..} =
_testAssertion = Steps $ regToCasmAssertion file' expected'
}
filterTests :: [String] -> [PosTest] -> [PosTest]
filterTests incl = filter (\PosTest {..} -> _name `elem` incl)
filterOutTests :: [String] -> [PosTest] -> [PosTest]
filterOutTests incl = filter (\PosTest {..} -> not (_name `elem` incl))
allTests :: TestTree
allTests =
testGroup
"CASM from JuvixReg translation positive tests"
"JuvixReg to CASM translation positive tests"
(map (mkTest . testDescr) tests)
tests :: [PosTest]

View File

@ -1,6 +1,8 @@
module Casm.Run.Base where
import Base
import Data.Aeson
import Juvix.Compiler.Casm.Data.Result qualified as Casm
import Juvix.Compiler.Casm.Error
import Juvix.Compiler.Casm.Interpreter
import Juvix.Compiler.Casm.Translation.FromSource
@ -8,9 +10,35 @@ import Juvix.Compiler.Casm.Validate
import Juvix.Data.Field
import Juvix.Data.PPOutput
import Juvix.Parser.Error
import Runtime.Base qualified as R
casmRunAssertion' :: LabelInfo -> Code -> Path Abs File -> (String -> IO ()) -> Assertion
casmRunAssertion' labi instrs expectedFile step =
casmRunVM' :: Path Abs Dir -> Path Abs File -> IO Text
casmRunVM' dirPath outputFile = do
dir <- getCurrentDir
setCurrentDir dirPath
out0 <- R.readProcess "run_cairo_vm.sh" [toFilePath outputFile] ""
setCurrentDir dir
return $ fromString $ unlines $ drop 1 $ lines (fromText out0)
casmRunVM :: LabelInfo -> Code -> Path Abs File -> (String -> IO ()) -> Assertion
casmRunVM labi instrs expectedFile step = do
step "Check run_cairo_vm.sh is on path"
assertCmdExists $(mkRelFile "run_cairo_vm.sh")
withTempDir'
( \dirPath -> do
step "Serialize to Cairo bytecode"
let res = run $ casmToCairo (Casm.Result labi instrs)
outputFile = dirPath <//> $(mkRelFile "out.json")
encodeFile (toFilePath outputFile) res
step "Run Cairo VM"
actualOutput <- casmRunVM' dirPath outputFile
step "Compare expected and actual program output"
expected <- readFile expectedFile
assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
)
casmRunAssertion' :: Bool -> LabelInfo -> Code -> Path Abs File -> (String -> IO ()) -> Assertion
casmRunAssertion' bRunVM labi instrs expectedFile step =
case validate labi instrs of
Left err -> do
assertFailure (show (pretty err))
@ -19,12 +47,13 @@ casmRunAssertion' labi instrs expectedFile step =
( \dirPath -> do
let outputFile = dirPath <//> $(mkRelFile "out.out")
step "Interpret"
r' <- doRun labi instrs
hout <- openFile (toFilePath outputFile) WriteMode
r' <- doRun hout labi instrs
case r' of
Left err -> do
hClose hout
assertFailure (show (pretty err))
Right value' -> do
hout <- openFile (toFilePath outputFile) WriteMode
hPrint hout value'
hClose hout
actualOutput <- readFile outputFile
@ -32,14 +61,16 @@ casmRunAssertion' labi instrs expectedFile step =
expected <- readFile expectedFile
assertEqDiffText ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected
)
when bRunVM $
casmRunVM labi instrs expectedFile step
casmRunAssertion :: Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion
casmRunAssertion mainFile expectedFile step = do
casmRunAssertion :: Bool -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion
casmRunAssertion bRunVM mainFile expectedFile step = do
step "Parse"
r <- parseFile mainFile
case r of
Left err -> assertFailure (show (pretty err))
Right (labi, instrs) -> casmRunAssertion' labi instrs expectedFile step
Right (labi, instrs) -> casmRunAssertion' bRunVM labi instrs expectedFile step
casmRunErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
casmRunErrorAssertion mainFile step = do
@ -53,7 +84,7 @@ casmRunErrorAssertion mainFile step = do
Left {} -> assertBool "" True
Right () -> do
step "Interpret"
r' <- doRun labi instrs
r' <- doRun stderr labi instrs
case r' of
Left _ -> assertBool "" True
Right _ -> assertFailure "no error"
@ -64,7 +95,8 @@ parseFile f = do
return (runParser f s)
doRun ::
Handle ->
LabelInfo ->
Code ->
IO (Either CasmError FField)
doRun labi instrs = catchRunErrorIO (runCode labi instrs)
doRun hout labi instrs = catchRunErrorIO (hRunCode hout labi instrs)

View File

@ -5,6 +5,7 @@ import Casm.Run.Base
data PosTest = PosTest
{ _name :: String,
_runVM :: Bool,
_relDir :: Path Rel Dir,
_file :: Path Rel File,
_expectedFile :: Path Rel File
@ -21,7 +22,7 @@ testDescr PosTest {..} =
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Steps $ casmRunAssertion file' expected'
_testAssertion = Steps $ casmRunAssertion _runVM file' expected'
}
filterTests :: [String] -> [PosTest] -> [PosTest]
@ -37,71 +38,85 @@ tests :: [PosTest]
tests =
[ PosTest
"Test001: Sum of numbers"
True
$(mkRelDir ".")
$(mkRelFile "test001.casm")
$(mkRelFile "out/test001.out"),
PosTest
"Test002: Factorial"
True
$(mkRelDir ".")
$(mkRelFile "test002.casm")
$(mkRelFile "out/test002.out"),
PosTest
"Test003: Direct call"
True
$(mkRelDir ".")
$(mkRelFile "test003.casm")
$(mkRelFile "out/test003.out"),
PosTest
"Test004: Indirect call"
True
$(mkRelDir ".")
$(mkRelFile "test004.casm")
$(mkRelFile "out/test004.out"),
PosTest
"Test005: Exp function"
True
$(mkRelDir ".")
$(mkRelFile "test005.casm")
$(mkRelFile "out/test005.out"),
PosTest
"Test006: Branch"
True
$(mkRelDir ".")
$(mkRelFile "test006.casm")
$(mkRelFile "out/test006.out"),
PosTest
"Test007: Closure extension"
True
$(mkRelDir ".")
$(mkRelFile "test007.casm")
$(mkRelFile "out/test007.out"),
PosTest
"Test008: Integer arithmetic"
False -- integer division not yet supported
$(mkRelDir ".")
$(mkRelFile "test008.casm")
$(mkRelFile "out/test008.out"),
PosTest
"Test009: Recursion"
True
$(mkRelDir ".")
$(mkRelFile "test009.casm")
$(mkRelFile "out/test009.out"),
PosTest
"Test010: Functions returning functions"
True
$(mkRelDir ".")
$(mkRelFile "test010.casm")
$(mkRelFile "out/test010.out"),
PosTest
"Test011: Lists"
True
$(mkRelDir ".")
$(mkRelFile "test011.casm")
$(mkRelFile "out/test011.out"),
PosTest
"Test012: Recursion through higher-order functions"
True
$(mkRelDir ".")
$(mkRelFile "test012.casm")
$(mkRelFile "out/test012.out"),
PosTest
"Test013: Currying and uncurrying"
True
$(mkRelDir ".")
$(mkRelFile "test013.casm")
$(mkRelFile "out/test013.out"),
PosTest
"Test014: Field arithmetic"
False -- different textual representation of "negative" field elements
$(mkRelDir ".")
$(mkRelFile "test014.casm")
$(mkRelFile "out/test014.out")

View File

@ -9,8 +9,10 @@ import Juvix.Compiler.Reg.Transformation
import Juvix.Compiler.Reg.Translation.FromSource
import Juvix.Data.PPOutput
runAssertion :: Handle -> Symbol -> InfoTable -> IO ()
runAssertion hout sym tab = do
runAssertion :: Path Abs Dir -> Path Abs File -> Symbol -> InfoTable -> (String -> IO ()) -> Assertion
runAssertion _ outputFile sym tab step = do
hout <- openFile (toFilePath outputFile) WriteMode
step "Interpret"
r' <- doRun hout tab (lookupFunInfo tab sym)
case r' of
Left err -> do
@ -18,23 +20,23 @@ runAssertion hout sym tab = do
assertFailure (show (pretty err))
Right value' -> do
case value' of
ValVoid -> return ()
_ -> hPutStrLn hout (ppPrint tab value')
ValVoid ->
hClose hout
_ -> do
hPutStrLn hout (ppPrint tab value')
hClose hout
regRunAssertion' :: InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion
regRunAssertion' = regRunAssertionParam' runAssertion
regRunAssertionParam' :: (Handle -> Symbol -> InfoTable -> IO ()) -> InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion
regRunAssertionParam' :: (Path Abs Dir -> Path Abs File -> Symbol -> InfoTable -> (String -> IO ()) -> Assertion) -> InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion
regRunAssertionParam' interpretFun tab expectedFile step = do
case tab ^. infoMainFunction of
Just sym -> do
withTempDir'
( \dirPath -> do
let outputFile = dirPath <//> $(mkRelFile "out.out")
hout <- openFile (toFilePath outputFile) WriteMode
step "Interpret"
interpretFun hout sym tab
hClose hout
interpretFun dirPath outputFile sym tab step
actualOutput <- readFile outputFile
step "Compare expected and actual program output"
expected <- readFile expectedFile
@ -45,7 +47,7 @@ regRunAssertionParam' interpretFun tab expectedFile step = do
regRunAssertion :: Path Abs File -> Path Abs File -> [TransformationId] -> (InfoTable -> Assertion) -> (String -> IO ()) -> Assertion
regRunAssertion = regRunAssertionParam runAssertion
regRunAssertionParam :: (Handle -> Symbol -> InfoTable -> IO ()) -> Path Abs File -> Path Abs File -> [TransformationId] -> (InfoTable -> Assertion) -> (String -> IO ()) -> Assertion
regRunAssertionParam :: (Path Abs Dir -> Path Abs File -> Symbol -> InfoTable -> (String -> IO ()) -> Assertion) -> Path Abs File -> Path Abs File -> [TransformationId] -> (InfoTable -> Assertion) -> (String -> IO ()) -> Assertion
regRunAssertionParam interpretFun mainFile expectedFile trans testTrans step = do
step "Parse"
r <- parseFile mainFile

View File

@ -10,11 +10,11 @@ calculate:
ret
main:
-- 1 local variable
ap += 1
call get_regs
[fp] = [ap - 2] + 2
[ap] = calculate; ap++
-- [fp + 4] = closure pointer
[ap] = [ap - 2] + 3; ap++
-- FUID(calculate) = 1
[ap] = 1; ap++
-- 9 - stored args num
[ap] = 7; ap++
-- 9 - argsnum (remaining expected)
@ -23,7 +23,7 @@ main:
[ap] = 5; ap++
[ap] = 3; ap++
[ap] = 2; ap++
[ap] = [fp]; ap++
[ap] = [fp + 4]; ap++
call call_closure
ret
@ -35,9 +35,6 @@ get_ap_reg:
-- [fp - 3]: closure; [fp - 3 - k]: argument k to closure call
call_closure:
ap += 1
-- closure addr
[fp] = [[fp - 3]]
-- jmp rel (9 - argsnum)
jmp rel [[fp - 3] + 2]
[ap] = [fp - 11]; ap++
@ -58,7 +55,8 @@ call_closure:
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call [fp]
jmp rel [[fp - 3]]
call calculate
ret
end:

View File

@ -22,6 +22,14 @@ f:
call app_1
ret
ff:
[ap] = [fp - 3]; ap++
call ext_10
call app_1
-- [ap] = [[ap - 1]]; ap++
ret
plus:
[ap] = [fp - 3] + [fp - 4]; ap++
ret
@ -41,47 +49,59 @@ g:
ret
main:
ap += 3
-- calloc plus 0
call get_regs
[ap] = plus; ap++
[ap] = 1; ap++
[ap] = 9; ap++
[ap] = 7; ap++
[ap] = [ap - 5] + 2; ap++
call f
-- 11
[fp] = [ap - 1]
call rel 3
nop
ret
-- [fp - 3] = 11
-- calloc minus 0
call get_regs
[ap] = minus; ap++
[ap] = 4; ap++
[ap] = 9; ap++
[ap] = 7; ap++
[ap] = [ap - 5] + 2; ap++
call f
-- 9
[fp + 1] = [ap - 1]
[ap] = [fp - 3]; ap++
call rel 3
nop
ret
-- [fp - 4] = 9
-- [fp - 3] = 11
-- calloc mult 0
call get_regs
[ap] = mult; ap++
[ap] = 7; ap++
[ap] = 9; ap++
[ap] = 7; ap++
[ap] = [ap - 5] + 2; ap++
call f
-- 10
[ap] = [ap - 1] + [fp]; ap++
[fp + 2] = [ap - 1] + [fp + 1]
-- [fp + 2] = 30
[ap] = [fp - 4]; ap++
[ap] = [fp - 3]; ap++
call rel 3
nop
ret
-- [fp - 5] = 10
-- [fp - 4] = 9
-- [fp - 3] = 11
[ap] = [fp - 5] + [fp - 4]; ap++
[ap] = [ap - 1] + [fp - 3]; ap++
-- [fp + 1] = 30
-- calloc g 2
call get_regs
[ap] = g; ap++
[ap] = 10; ap++
[ap] = 7; ap++
[ap] = 7; ap++
[ap] = 3; ap++
[ap] = 2; ap++
[ap] = [ap - 7] + 2; ap++
call f
call ff
-- 11
[ap] = [fp + 2] + [ap - 1]; ap++
[ap] = [fp + 1] + [ap - 1]; ap++
ret
-- result: 41
@ -91,11 +111,65 @@ get_regs:
get_ap_reg:
ret
-- [fp - 3]: closure; [fp - 4]: argument
extend_closure_1:
-- copy stored args reversing them
jmp rel [[fp - 3] + 1]
[ap] = [[fp - 3] + 10]; ap++
[ap] = [[fp - 3] + 9]; ap++
[ap] = [[fp - 3] + 8]; ap++
[ap] = [[fp - 3] + 7]; ap++
[ap] = [[fp - 3] + 6]; ap++
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
[ap] = 10; ap++
[ap] = [[fp - 3] + 1]; ap++
[ap] = [ap - 2] - [ap - 1]; ap++
jmp rel [ap - 1]
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
-- now ap = fp + 11
-- alloc closure header
call get_regs
-- now ap = fp + 15
-- [fp + 15] = closure pointer
[ap] = [ap - 2] + 7; ap++
-- [fp + 16] = 9 - sargs
[ap] = [[fp - 3] + 1]; ap++
-- [fp + 17] = 9 - argsnum (expected)
[ap] = [[fp - 3] + 2]; ap++
-- [fp + 18] = 9
[ap] = 9; ap++
-- [fp + 19] = sargs
[ap] = [fp + 18] - [fp + 16]; ap++
[ap] = [[fp - 3]]; ap++
[ap] = [fp + 16] - 1; ap++
[ap] = [fp + 17] + 1; ap++
-- end alloc closure header
-- jmp rel (9 - sargs)
jmp rel [fp + 16]
[ap] = [fp + 7]; ap++
[ap] = [fp + 6]; ap++
[ap] = [fp + 5]; ap++
[ap] = [fp + 4]; ap++
[ap] = [fp + 3]; ap++
[ap] = [fp + 2]; ap++
[ap] = [fp + 1]; ap++
[ap] = [fp]; ap++
-- extra args
[ap] = [fp - 4]; ap++
[ap] = [fp + 15]; ap++
ret
-- [fp - 3]: closure; [fp - 3 - k]: argument k to closure call
call_closure:
ap += 1
-- closure addr
[fp] = [[fp - 3]]
-- jmp rel (9 - argsnum)
jmp rel [[fp - 3] + 2]
[ap] = [fp - 11]; ap++
@ -116,47 +190,18 @@ call_closure:
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call [fp]
jmp rel [[fp - 3]]
call plus
ret
-- [fp - 3]: closure; [fp - 4]: argument
extend_closure_1:
ap += 5
-- 9 - sargs
[fp + 1] = [[fp - 3] + 1]
-- 9 - argsnum (expected)
[fp + 2] = [[fp - 3] + 2]
[fp + 3] = 9
-- [fp + 4] = sargs
[fp + 4] = [fp + 3] - [fp + 1]
-- copy stored args reversing them
jmp rel [fp + 1]
[ap] = [[fp - 3] + 10]; ap++
[ap] = [[fp - 3] + 9]; ap++
[ap] = [[fp - 3] + 8]; ap++
[ap] = [[fp - 3] + 7]; ap++
[ap] = [[fp - 3] + 6]; ap++
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call get_regs
[fp] = [ap - 2] + 2
[ap] = [[fp - 3]]; ap++
[ap] = [fp + 1] - 1; ap++
[ap] = [fp + 2] + 1; ap++
-- jmp rel (9 - sargs)
jmp rel [fp + 1]
[ap] = [fp + 11]; ap++
[ap] = [fp + 10]; ap++
[ap] = [fp + 9]; ap++
[ap] = [fp + 8]; ap++
[ap] = [fp + 8]; ap++
[ap] = [fp + 7]; ap++
[ap] = [fp + 6]; ap++
[ap] = [fp + 5]; ap++
-- extra args
[ap] = [fp - 4]; ap++
[ap] = [fp]; ap++
nop
call minus
ret
nop
call mult
ret
nop
call g
ret
nop
end:

View File

@ -9,21 +9,23 @@ func:
ret
main:
ap += 2
[ap] = 5; ap++
[ap] = 17; ap++
[ap] = [ap - 1] idiv [ap - 2]; ap++
call func
[fp] = [ap - 1] -- -1
call rel 3
nop
ret
-- [fp - 3] = -1
[ap] = 5; ap++
[ap] = 0; ap++
[ap] = [ap - 1] imul [ap - 2]; ap++
[fp + 1] = [ap - 1] ilt 1 -- true = 0
[ap] = [fp] imul 7; ap++
[ap] = [ap - 1] ilt 1; ap++ -- [fp + 3] = true = 0
[ap] = [fp - 3] imul 7; ap++
[ap] = [ap - 1] idiv 3; ap++
[ap] = [ap - 1] iadd 2; ap++
[ap] = [ap - 1] iadd [fp]; ap++
[ap] = [ap - 1] iadd [fp + 1]; ap++
[ap] = [ap - 1] iadd [fp - 3]; ap++
[ap] = [ap - 1] iadd [fp + 3]; ap++
[ap] = [ap - 1] iadd 1; ap++
ret

View File

@ -15,73 +15,83 @@ g:
ret
f:
ap += 1
[ap] = [fp - 3] - 6; ap++
jmp f_label_1 if [ap - 1] != 0
call get_regs
[fp] = [ap - 2] + 2
[ap] = const; ap++
-- calloc const
[ap] = 1; ap++
[ap] = 8; ap++
[ap] = 8; ap++
[ap] = 0; ap++
[ap] = [fp]; ap++
[ap] = [ap - 6] + 2; ap++
ret
f_label_1:
[ap] = [fp - 3] - 5; ap++
jmp f_label_2 if [ap - 1] != 0
call get_regs
[fp] = [ap - 2] + 2
[ap] = const; ap++
-- calloc const
[ap] = 1; ap++
[ap] = 8; ap++
[ap] = 8; ap++
[ap] = 1; ap++
[ap] = [fp]; ap++
[ap] = [ap - 6] + 2; ap++
ret
f_label_2:
[ap] = [fp - 3] - 10; ap++
jmp f_label_3 if [ap - 1] != 0
call get_regs
[fp] = [ap - 2] + 2
[ap] = g; ap++
-- calloc g
[ap] = 4; ap++
[ap] = 9; ap++
[ap] = 8; ap++
[ap] = [fp]; ap++
[ap] = [ap - 5] + 2; ap++
ret
f_label_3:
call get_regs
[fp] = [ap - 2] + 2
[ap] = id; ap++
-- calloc id
[ap] = 7; ap++
[ap] = 9; ap++
[ap] = 8; ap++
[ap] = [fp]; ap++
[ap] = [ap - 5] + 2; ap++
ret
main:
ap += 3
[ap] = 5; ap++
call f
[ap] = 6; ap++
[ap] = [ap - 2]; ap++
call call_closure
[fp] = [ap - 1]
call rel 3
ret
nop
-- [fp - 3] = closure call result
[ap] = 6; ap++
call f
[ap] = 5; ap++
[ap] = [ap - 2]; ap++
call call_closure
[fp + 1] = [ap - 1] + [fp]
[ap] = [fp - 3]; ap++
call rel 3
ret
nop
-- [fp] = sum
[ap] = [fp - 3] + [fp - 4]; ap++
[ap] = 10; ap++
call f
[ap] = 5; ap++
[ap] = [ap - 2]; ap++
call call_closure
[fp + 2] = [ap - 1] + [fp + 1]
[ap] = [fp]; ap++
call rel 3
ret
nop
[ap] = [fp - 3] + [fp - 4]; ap++
[ap] = 11; ap++
call f
[ap] = 5; ap++
[ap] = [ap - 2]; ap++
call call_closure
[ap] = [ap - 1] + [fp + 2]; ap++
[ap] = [ap - 1] + [fp]; ap++
ret
get_regs:
@ -92,9 +102,6 @@ get_ap_reg:
-- [fp - 3]: closure; [fp - 3 - k]: argument k to closure call
call_closure:
ap += 1
-- closure addr
[fp] = [[fp - 3]]
-- jmp rel (9 - argsnum)
jmp rel [[fp - 3] + 2]
[ap] = [fp - 11]; ap++
@ -115,7 +122,14 @@ call_closure:
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call [fp]
jmp rel [[fp - 3]]
call const
ret
nop
call g
ret
nop
call id
ret
end:

View File

@ -25,26 +25,33 @@ null_cons:
ret
map:
ap += 2
[ap] = [[fp - 4]]; ap++
jmp map_cons if [ap - 1] != 0
[ap] = [fp - 4]; ap++
[fp] = 0
[fp + 1] = 0
ret
map_cons:
[ap] = [[fp - 4] + 2]; ap++
[ap] = [fp - 3]; ap++
call map
[fp] = [ap - 1]
[ap] = [fp - 4]; ap++
[ap] = [fp - 3]; ap++
call rel 3
ret
nop
-- [fp - 5] = mapped tail
[ap] = [[fp - 4] + 1]; ap++
[ap] = [fp - 3]; ap++
call call_closure
[fp + 1] = [ap - 1]
[ap] = [fp - 5]; ap++
call rel 3
ret
nop
-- [fp - 4] = mapped head
-- [fp - 3] = mapped tail
call get_regs
[ap] = 1; ap++
[ap] = [fp + 1]; ap++
[ap] = [fp]; ap++
[ap] = [fp - 4]; ap++
[ap] = [fp - 3]; ap++
[ap] = [ap - 5] + 2; ap++
ret
@ -65,41 +72,55 @@ sum_label_1:
ret
main:
ap += 6
call get_regs
[fp] = [ap - 2] + 2
-- [fp + 4] = nil
[ap] = [ap - 2] + 3; ap++
[ap] = 0; ap++
call get_regs
[fp + 1] = [ap - 2] + 2
-- [fp + 10]
[ap] = [ap - 2] + 3; ap++
[ap] = 1; ap++
[ap] = 1; ap++
[ap] = [fp]; ap++
[ap] = [fp + 4]; ap++
call get_regs
[fp + 2] = [ap - 2] + 2
-- [fp + 18]
[ap] = [ap - 2] + 3; ap++
[ap] = 1; ap++
[ap] = 0; ap++
[ap] = [fp + 1]; ap++
-- tmp[0] == [fp + 2]
[ap] = [fp + 2]; ap++
[ap] = [fp + 10]; ap++
-- tmp[0] == [fp + 18]
[ap] = [fp + 18]; ap++
call null
[fp + 3] = [ap - 1]
[ap] = [fp + 2]; ap++
[ap] = [fp + 18]; ap++
call rel 3
ret
nop
[ap] = [fp - 3]; ap++
call tl
call tl
call null
[fp + 4] = [fp + 3] + [ap - 1]
[ap] = [fp + 2]; ap++
[ap] = [fp - 4] + [ap - 1]; ap++
[ap] = [fp - 3]; ap++
call rel 3
ret
nop
[ap] = [fp - 3]; ap++
call hd
[fp + 5] = [fp + 4] + [ap - 1]
[ap] = [fp - 4] + [ap - 1]; ap++
[ap] = [fp - 3]; ap++
call rel 3
ret
nop
call get_regs
[ap] = add_one; ap++
-- calloc add_one
[ap] = 1; ap++
[ap] = 9; ap++
[ap] = 8; ap++
[ap] = [fp + 2]; ap++
[ap] = [fp - 3]; ap++
[ap] = [ap - 6] + 2; ap++
call map
call sum
[ap] = [fp + 5] + [ap - 1]; ap++
[ap] = [fp - 4] + [ap - 1]; ap++
ret
get_regs:
@ -110,9 +131,6 @@ get_ap_reg:
-- [fp - 3]: closure; [fp - 3 - k]: argument k to closure call
call_closure:
ap += 1
-- closure addr
[fp] = [[fp - 3]]
-- jmp rel (9 - argsnum)
jmp rel [[fp - 3] + 2]
[ap] = [fp - 11]; ap++
@ -133,7 +151,8 @@ call_closure:
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call [fp]
jmp rel [[fp - 3]]
call add_one
ret
end:

View File

@ -16,7 +16,8 @@ g_label_1:
f:
call get_regs
[ap] = f; ap++
-- calloc f
[ap] = 1; ap++
[ap] = 9; ap++
[ap] = 8; ap++
[ap] = [fp - 3]; ap++
@ -38,9 +39,6 @@ get_ap_reg:
-- [fp - 3]: closure; [fp - 3 - k]: argument k to closure call
call_closure:
ap += 1
-- closure addr
[fp] = [[fp - 3]]
-- jmp rel (9 - argsnum)
jmp rel [[fp - 3] + 2]
[ap] = [fp - 11]; ap++
@ -61,7 +59,8 @@ call_closure:
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call [fp]
jmp rel [[fp - 3]]
call f
ret
end:

View File

@ -23,7 +23,8 @@ inc:
h:
call get_regs
[ap] = inc; ap++
-- calloc inc
[ap] = 1; ap++
[ap] = 9; ap++
[ap] = 8; ap++
[ap] = [ap - 5] + 2; ap++
@ -39,7 +40,8 @@ capp:
curry:
call get_regs
[ap] = capp; ap++
-- calloc capp
[ap] = 4; ap++
[ap] = 8; ap++
[ap] = 8; ap++
[ap] = [fp - 3]; ap++
@ -57,7 +59,8 @@ uapp:
uncurry:
call get_regs
[ap] = uapp; ap++
-- calloc uapp
[ap] = 7; ap++
[ap] = 8; ap++
[ap] = 7; ap++
[ap] = [fp - 3]; ap++
@ -65,25 +68,32 @@ uncurry:
ret
main:
ap += 4
call get_regs
[fp] = [ap - 2] + 2
[ap] = inc; ap++
-- [fp + 4]
[ap] = [ap - 2] + 3; ap++
-- calloc inc
[ap] = 1; ap++
[ap] = 9; ap++
[ap] = 8; ap++
call get_regs
[ap] = app; ap++
-- [fp + 12]
[ap] = [ap - 2] + 3; ap++
-- calloc app
[ap] = 10; ap++
[ap] = 9; ap++
[ap] = 7; ap++
[ap] = 5; ap++
[ap] = [fp]; ap++
[ap] = [ap - 7] + 2; ap++
[ap] = [fp + 4]; ap++
call app'
[fp + 2] = [ap - 1]
call rel 3
ret
nop
-- [fp - 3]
call get_regs
[ap] = app; ap++
-- calloc app
[ap] = 10; ap++
[ap] = 9; ap++
[ap] = 7; ap++
[ap] = [ap - 5] + 2; ap++
@ -91,26 +101,34 @@ main:
[ap] = 4; ap++
[ap] = [ap - 2]; ap++
call call_closure
[fp + 3] = [fp + 2] + [ap - 1]
[ap] = [fp - 3] + [ap - 1]; ap++
call rel 3
ret
nop
-- uncurry (curry app) inc 7
call get_regs
[ap] = app; ap++
-- calloc app
[ap] = 10; ap++
[ap] = 9; ap++
[ap] = 7; ap++
[ap] = [ap - 5] + 2; ap++
call curry
call uncurry
[fp + 1] = [ap - 1]
[ap] = [fp - 3]; ap++
call rel 3
ret
nop
call get_regs
[ap] = inc; ap++
-- calloc inc
[ap] = 1; ap++
[ap] = 9; ap++
[ap] = 8; ap++
[ap] = 7; ap++
[ap] = [ap - 6] + 2; ap++
[ap] = [fp + 1]; ap++
[ap] = [fp - 4]; ap++
call call_closure
[ap] = [fp + 3] + [ap - 1]; ap++
[ap] = [fp - 3] + [ap - 1]; ap++
ret
get_regs:
@ -121,9 +139,6 @@ get_ap_reg:
-- [fp - 3]: closure; [fp - 3 - k]: argument k to closure call
call_closure:
ap += 1
-- closure addr
[fp] = [[fp - 3]]
-- jmp rel (9 - argsnum)
jmp rel [[fp - 3] + 2]
[ap] = [fp - 11]; ap++
@ -144,21 +159,24 @@ call_closure:
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
call [fp]
jmp rel [[fp - 3]]
call inc
ret
nop
call capp
ret
nop
call uapp
ret
nop
call app
ret
nop
-- [fp - 3]: closure; [fp - 4]: argument
extend_closure_1:
ap += 5
-- 9 - sargs
[fp + 1] = [[fp - 3] + 1]
-- 9 - argsnum (expected)
[fp + 2] = [[fp - 3] + 2]
[fp + 3] = 9
-- [fp + 4] = sargs
[fp + 4] = [fp + 3] - [fp + 1]
-- copy stored args reversing them
jmp rel [fp + 1]
jmp rel [[fp - 3] + 1]
[ap] = [[fp - 3] + 10]; ap++
[ap] = [[fp - 3] + 9]; ap++
[ap] = [[fp - 3] + 8]; ap++
@ -167,24 +185,49 @@ extend_closure_1:
[ap] = [[fp - 3] + 5]; ap++
[ap] = [[fp - 3] + 4]; ap++
[ap] = [[fp - 3] + 3]; ap++
[ap] = 10; ap++
[ap] = [[fp - 3] + 1]; ap++
[ap] = [ap - 2] - [ap - 1]; ap++
jmp rel [ap - 1]
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
[ap] = [ap - 1]; ap++
-- now ap = fp + 11
-- alloc closure header
call get_regs
[fp] = [ap - 2] + 2
-- now ap = fp + 15
-- [fp + 15] = closure pointer
[ap] = [ap - 2] + 7; ap++
-- [fp + 16] = 9 - sargs
[ap] = [[fp - 3] + 1]; ap++
-- [fp + 17] = 9 - argsnum (expected)
[ap] = [[fp - 3] + 2]; ap++
-- [fp + 18] = 9
[ap] = 9; ap++
-- [fp + 19] = sargs
[ap] = [fp + 18] - [fp + 16]; ap++
[ap] = [[fp - 3]]; ap++
[ap] = [fp + 1] - 1; ap++
[ap] = [fp + 2] + 1; ap++
[ap] = [fp + 16] - 1; ap++
[ap] = [fp + 17] + 1; ap++
-- end alloc closure header
-- jmp rel (9 - sargs)
jmp rel [fp + 1]
[ap] = [fp + 11]; ap++
[ap] = [fp + 10]; ap++
[ap] = [fp + 9]; ap++
[ap] = [fp + 8]; ap++
[ap] = [fp + 8]; ap++
jmp rel [fp + 16]
[ap] = [fp + 7]; ap++
[ap] = [fp + 6]; ap++
[ap] = [fp + 5]; ap++
[ap] = [fp + 4]; ap++
[ap] = [fp + 3]; ap++
[ap] = [fp + 2]; ap++
[ap] = [fp + 1]; ap++
[ap] = [fp]; ap++
-- extra args
[ap] = [fp - 4]; ap++
[ap] = [fp]; ap++
[ap] = [fp + 15]; ap++
ret
end: