VampIR range checks and error handling

app/Commands/Dev/Core/Compile/Base.hs

@@ -25,6 +25,7 @@ getEntry PipelineArg {..} = do
     ep
       { _entryPointTarget = getTarget (_pipelineArgOptions ^. compileTarget),
         _entryPointDebug = _pipelineArgOptions ^. compileDebug,
+        _entryPointUnsafe = _pipelineArgOptions ^. compileUnsafe,
         _entryPointOptimizationLevel = fromMaybe defaultOptLevel (_pipelineArgOptions ^. compileOptimizationLevel),
         _entryPointInliningDepth = _pipelineArgOptions ^. compileInliningDepth
       }

app/Commands/Extra/Compile/Options.hs

@@ -28,6 +28,7 @@ data CompileOptions = CompileOptions
     _compilePreprocess :: Bool,
     _compileAssembly :: Bool,
     _compileTerm :: Bool,
+    _compileUnsafe :: Bool,
     _compileOutputFile :: Maybe (AppPath File),
     _compileTarget :: CompileTarget,
     _compileInputFile :: Maybe (AppPath File),
@@ -82,6 +83,15 @@ parseCompileOptions supportedTargets parseInputFile = do
               )
         | otherwise ->
             pure False
+  _compileUnsafe <-
+    if
+        | elem TargetVampIR supportedTargets ->
+            switch
+              ( long "unsafe"
+                  <> help "Disable range and error checking (for targets: vampir)"
+              )
+        | otherwise ->
+            pure False
   _compileOptimizationLevel <-
     optional
       ( option

runtime/src/vampir/stdlib.pir

@@ -1,47 +1,88 @@
+////////////////////////////////////////////////
+// VampIR runtime for Juvix (safe version)
+////////////////////////////////////////////////
+
+def fst (x, y) = x;
+def snd (x, y) = y;
+
 def isBool x = (x * (x - 1) = 0);
 
+def isZero x = {
+    def xi = fresh (1 | x);
+    def y = 1 - xi * x;
+    x * y = 0;
+    y
+};
+
 def msb_rec x = {
     def x0 = fresh (x%2); isBool x0;
     def x1 = fresh (x\2);
     x = x0 + 2*x1;
     x1
 };
 
-def msb n x = {
-    def b = iter (n - 1) msb_rec x;
-    isBool b;
-    b
+def msb n x = iter (n - 1) msb_rec x;
+
+def isNegative x = {
+    def b = msb integerBits (x + 2^(integerBits - 1));
+    def c = 1 - b;
+    (c, isZero (b * c))
+};
+def isNegativeD x = {
+    def b = msb (2*integerBits) (x + 2^(2*integerBits - 1));
+    def c = 1 - b;
+    (c, isZero (b * c))
 };
 
-def isNegative x = 1 - msb integerBits (x + 2^(integerBits - 1));
-def isNegativeD x = 1 - msb (2*integerBits) (x + 2^(2*integerBits - 1));
+def range_check x = {
+    def b = msb integerBits (x + 2^(integerBits - 1));
+    isZero (b * (b - 1))
+};
+
+def divRem a b = {
+    def q = fresh (a\b);
+    def r = fresh (a%b);
+    def (r1, e1) = isNegative r;
+    def (r2, e2) = isNegative (r - b);
+    r1 = 0;
+    r2 = 1;
+    a = b * q + r;
+    (q, r, e1 * e2)
+};
 
-def add x y = x + y;
-def sub x y = x - y;
-def mul x y = x * y;
+def number x = (x + 0, 1);
+def fail = (0, 0);
 
-def isZero x = {
-    def xi = fresh (1 | x);
-    x * (1 - xi * x) = 0;
-    1 - xi * x
+def add (x, e1) (y, e2) = {
+    (x + y, e1 * e2 * range_check (x + y))
+};
+def sub (x, e1) (y, e2) = {
+    (x - y, e1 * e2 * range_check (x - y))
+};
+def mul (x, e1) (y, e2) = {
+    (x * y, e1 * e2 * range_check (x * y))
 };
-def equal x y = isZero (x - y);
 
-def if b x y = b * x + (1 - b) * y;
+def equal (x, e1) (y, e2) = (isZero (x - y), e1 * e2);
 
-def lessThan x y = isNegativeD (x - y);
-def lessOrEqual x y = lessThan x (y + 1);
+def if (b, e) (x, e1) (y, e2) = (b * x + (1 - b) * y, e * (b * e1 + (1 - b) * e2));
 
-def divRem a b = {
-    def q = fresh (a\b);
-    def r = fresh (a%b);
-    isNegative r = 0;
-    lessThan r b = 1;
-    a = b * q + r; (q, r)
+def lessThan (x, e1) (y, e2) = {
+    def (z, e) = isNegativeD (x - y);
+    (z, e1 * e2 * e)
+};
+def lessOrEqual (x, e1) (y, e2) = {
+    def (z, e) = isNegativeD (x - y - 1);
+    (z, e1 * e2 * e)
 };
 
-def fst (x, y) = x;
-def snd (x, y) = y;
+def div (x, e1) (y, e2) = {
+    def (z, _, e) = (divRem x y);
+    (z, e1 * e2 * e)
+};
+def rem (x, e1) (y, e2) = {
+    def (_, z, e) = divRem x y;
+    (z, e1 * e2 * e)
+};
 
-def div x y = fst (divRem x y);
-def rem x y = snd (divRem x y);
+////////////////////////////////////////////////

runtime/src/vampir/stdlib_unsafe.pir

@@ -0,0 +1,54 @@
+////////////////////////////////////////////////
+// VampIR runtime for Juvix (unsafe version)
+////////////////////////////////////////////////
+
+def fst (x, y) = x;
+def snd (x, y) = y;
+
+def isBool x = (x * (x - 1) = 0);
+
+def msb_rec x = {
+    def x0 = fresh (x%2); isBool x0;
+    def x1 = fresh (x\2);
+    x = x0 + 2*x1;
+    x1
+};
+
+def msb n x = iter (n - 1) msb_rec x;
+
+def isNegative x = 1 - msb integerBits (x + 2^(integerBits - 1));
+def isNegativeD x = 1 - msb (2*integerBits) (x + 2^(2*integerBits - 1));
+
+def isZero x = {
+    def xi = fresh (1 | x);
+    def y = 1 - xi * x;
+    x * y = 0;
+    y
+};
+
+def divRem a b = {
+    def q = fresh (a\b);
+    def r = fresh (a%b);
+    isNegative r = 0;
+    isNegativeD (r - b) = 1;
+    a = b * q + r; (q, r)
+};
+
+def number x = x + 0;
+def fail = 0;
+
+def add x y = x + y;
+def sub x y = x - y;
+def mul x y = x * y;
+
+def equal x y = isZero (x - y);
+
+def if b x y = b * x + (1 - b) * y;
+
+def lessThan x y = isNegativeD (x - y);
+def lessOrEqual x y = lessThan x (y + 1);
+
+def div x y = fst (divRem x y);
+def rem x y = snd (divRem x y);
+
+////////////////////////////////////////////////

src/Juvix/Compiler/Backend/VampIR/Language.hs

@@ -78,7 +78,7 @@ instance HasAtomicity IfThenElse where
 instance HasAtomicity Expression where
   atomicity = \case
     ExpressionVar x -> atomicity x
-    ExpressionConstant {} -> Atom
+    ExpressionConstant {} -> Aggregate appFixity
     ExpressionBinop x -> atomicity x
     ExpressionIfThenElse x -> atomicity x
     ExpressionFail -> Atom

src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs

@@ -51,10 +51,10 @@ instance PrettyCode IfThenElse where
 instance PrettyCode Expression where
   ppCode = \case
     ExpressionVar x -> ppCode x
-    ExpressionConstant i -> return $ annotate AnnLiteralInteger (pretty i)
+    ExpressionConstant i -> return $ kwNumber <+> annotate AnnLiteralInteger (pretty i)
     ExpressionBinop x -> ppCode x
     ExpressionIfThenElse x -> ppCode x
-    ExpressionFail -> return $ annotate AnnLiteralInteger "0"
+    ExpressionFail -> return kwFail
 
 instance PrettyCode LocalDef where
   ppCode LocalDef {..} = do
@@ -72,10 +72,10 @@ instance PrettyCode Function where
 
 ppEquation :: Function -> Sem r (Doc Ann)
 ppEquation Function {..} = do
-  let args = map (\arg -> "(" <> pretty arg <> " + 0)") _functionInputs
+  let args = map (\arg -> parens (kwNumber <+> pretty arg)) _functionInputs
       out = pretty _functionOutput
   fn <- ppName KNameFunction _functionName
-  return $ fn <+> hsep args <+> kwEq <+> "(" <> out <> " + 0)" <> semi
+  return $ fn <+> hsep args <+> kwEq <+> parens (kwNumber <+> out) <> semi
 
 ppPub :: Text -> Sem r (Doc Ann)
 ppPub p = return $ "pub " <> pretty p <> semi
@@ -86,18 +86,23 @@ instance PrettyCode Program where
     fns <- mapM ppCode _programFunctions
     eqns <- mapM ppEquation _programFunctions
     bits <- asks (^. optIntegerBits)
-    return $ vsep pubs <> line <> line <> pretty (vampIRDefs bits) <> line <> line <> vsep fns <> line <> line <> vsep eqns
+    unsafe <- asks (^. optUnsafe)
+    return $ vsep pubs <> line <> line <> pretty (vampIRDefs bits unsafe) <> line <> line <> vsep fns <> line <> line <> vsep eqns
 
 --------------------------------------------------------------------------------
 -- VampIR definitions
 --------------------------------------------------------------------------------
 
-vampIRDefs :: Int -> String
-vampIRDefs bits =
+vampIRDefs :: Int -> Bool -> String
+vampIRDefs bits unsafe =
   "def integerBits = "
     <> show bits
-    <> ";\n"
-    <> UTF8.toString $(FE.makeRelativeToProject "runtime/src/vampir/stdlib.pir" >>= FE.embedFile)
+    <> ";\n\n"
+    <> if
+        | unsafe ->
+            UTF8.toString $(FE.makeRelativeToProject "runtime/src/vampir/stdlib_unsafe.pir" >>= FE.embedFile)
+        | otherwise ->
+            UTF8.toString $(FE.makeRelativeToProject "runtime/src/vampir/stdlib.pir" >>= FE.embedFile)
 
 --------------------------------------------------------------------------------
 -- helper functions

src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs

@@ -10,6 +10,12 @@ kwDef = keyword Str.vampirDef
 kwEq :: Doc Ann
 kwEq = keyword Str.vampirEq
 
+kwNumber :: Doc Ann
+kwNumber = keyword Str.vampirNumber
+
+kwFail :: Doc Ann
+kwFail = keyword Str.vampirFail
+
 kwAdd :: Doc Ann
 kwAdd = keyword Str.vampirAdd
 

src/Juvix/Compiler/Backend/VampIR/Pretty/Options.hs

@@ -2,16 +2,18 @@ module Juvix.Compiler.Backend.VampIR.Pretty.Options where
 
 import Juvix.Prelude
 
-newtype Options = Options
-  { _optIntegerBits :: Int
+data Options = Options
+  { _optIntegerBits :: Int,
+    _optUnsafe :: Bool
   }
 
 makeLenses ''Options
 
 defaultOptions :: Options
 defaultOptions =
   Options
-    { _optIntegerBits = 24
+    { _optIntegerBits = 24,
+      _optUnsafe = False
     }
 
 traceOptions :: Options

src/Juvix/Compiler/Backend/VampIR/Translation.hs

@@ -1,18 +1,29 @@
 module Juvix.Compiler.Backend.VampIR.Translation
   ( module Juvix.Compiler.Backend.VampIR.Translation,
-    module Juvix.Compiler.Backend.VampIR.Translation.FromCore,
   )
 where
 
 import Juvix.Compiler.Backend.VampIR.Language
 import Juvix.Compiler.Backend.VampIR.Pretty
-import Juvix.Compiler.Backend.VampIR.Translation.FromCore
+import Juvix.Compiler.Backend.VampIR.Translation.FromCore qualified as VampIR
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Pipeline.EntryPoint
 
 newtype Result = Result
   { _resultCode :: Text
   }
 
-toResult :: Program -> Result
-toResult p = Result $ ppPrint p
-
 makeLenses ''Result
+
+toResult :: Bool -> Program -> Result
+toResult unsafe p = Result $ show $ ppOut opts p
+  where
+    opts = defaultOptions {_optUnsafe = unsafe}
+
+fromCore :: (Member (Reader EntryPoint) r) => InfoTable -> Sem r Result
+fromCore tab = do
+  unsafe <- asks (^. entryPointUnsafe)
+  return $ toResult unsafe $ VampIR.fromCore tab
+
+fromCore' :: Bool -> InfoTable -> Result
+fromCore' unsafe = toResult unsafe . VampIR.fromCore

src/Juvix/Compiler/Pipeline.hs

@@ -143,7 +143,7 @@ coreToGeb :: (Members '[Error JuvixError, Reader EntryPoint] r) => Geb.ResultSpe
 coreToGeb spec = Core.toGeb >=> return . uncurry (Geb.toResult spec) . Geb.fromCore
 
 coreToVampIR :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.InfoTable -> Sem r VampIR.Result
-coreToVampIR = Core.toVampIR >=> return . VampIR.toResult . VampIR.fromCore
+coreToVampIR = Core.toVampIR >=> VampIR.fromCore
 
 asmToMiniC' :: (Members '[Error JuvixError, Reader Asm.Options] r) => Asm.InfoTable -> Sem r C.MiniCResult
 asmToMiniC' = mapError (JuvixError @Asm.AsmError) . Asm.toReg' >=> regToMiniC' . Reg.fromAsm
@@ -154,7 +154,7 @@ regToMiniC' tab = do
   return $ C.fromReg (e ^. Asm.optLimits) tab
 
 coreToVampIR' :: (Members '[Error JuvixError, Reader Core.CoreOptions] r) => Core.InfoTable -> Sem r VampIR.Result
-coreToVampIR' = Core.toVampIR' >=> return . VampIR.toResult . VampIR.fromCore
+coreToVampIR' = Core.toVampIR' >=> return . VampIR.fromCore' False
 
 --------------------------------------------------------------------------------
 -- Run pipeline

src/Juvix/Compiler/Pipeline/EntryPoint.hs

@@ -32,6 +32,7 @@ data EntryPoint = EntryPoint
     _entryPointStdin :: Maybe Text,
     _entryPointTarget :: Target,
     _entryPointDebug :: Bool,
+    _entryPointUnsafe :: Bool,
     _entryPointUnrollLimit :: Int,
     _entryPointOptimizationLevel :: Int,
     _entryPointInliningDepth :: Int,
@@ -78,6 +79,7 @@ defaultEntryPointNoFile roots =
       _entryPointGenericOptions = defaultGenericOptions,
       _entryPointTarget = TargetCore,
       _entryPointDebug = False,
+      _entryPointUnsafe = False,
       _entryPointUnrollLimit = defaultUnrollLimit,
       _entryPointOptimizationLevel = defaultOptimizationLevel,
       _entryPointInliningDepth = defaultInliningDepth,

src/Juvix/Extra/Strings.hs

@@ -683,6 +683,12 @@ vampirDef = "def"
 vampirEq :: (IsString s) => s
 vampirEq = "="
 
+vampirNumber :: (IsString s) => s
+vampirNumber = "number"
+
+vampirFail :: (IsString s) => s
+vampirFail = "fail"
+
 vampirAdd :: (IsString s) => s
 vampirAdd = "add"
 

test/VampIR/Core/Base.hs

@@ -52,7 +52,7 @@ vampirSetupArgs VampirPlonk dirPath step = do
         "plonk",
         "setup",
         "-m",
-        "8",
+        "9",
         "-o",
         toFilePath (dirPath <//> $(mkRelFile "params.pp"))
       ]