From 6bd8c5ee5c4a44ffffd62afb18a7d6f47b225454 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 20 Dec 2024 08:01:33 -0600 Subject: [PATCH 1/2] Support toSignedInteger in reference evaluator Checks off one box in #1249. --- CHANGES.md | 3 +++ src/Cryptol/Eval/Reference.lhs | 4 ++++ tests/issues/issue1249.icry | 12 ++++++++++++ tests/issues/issue1249.icry.stdout | 11 +++++++++++ 4 files changed, 30 insertions(+) create mode 100644 tests/issues/issue1249.icry create mode 100644 tests/issues/issue1249.icry.stdout diff --git a/CHANGES.md b/CHANGES.md index 11ffd01cd..ab73fa9a6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -15,6 +15,9 @@ were incorrectly computed. ([#1773](https://github.com/GaloisInc/cryptol/issues/1773)) +* The reference evaluator now evaluates the `toSignedInteger` primitive instead + of panicking. + ## New features * REPL command `:dumptests ` updated to write to stdout when diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 7edbfbdad..4ce7e99fb 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -758,6 +758,10 @@ by corresponding type classes: > , "lg2" ~> vFinPoly $ \n -> pure $ > VFun $ \v -> > vWord n <$> appOp1 lg2Wrap (fromVWord =<< v) +> , "toSignedInteger" +> ~> vFinPoly $ \_n -> pure $ +> VFun $ \x -> +> VInteger <$> (fromSignedVWord =<< x) > -- Rational > , "ratio" ~> VFun $ \l -> pure $ > VFun $ \r -> diff --git a/tests/issues/issue1249.icry b/tests/issues/issue1249.icry new file mode 100644 index 000000000..e89f65c3d --- /dev/null +++ b/tests/issues/issue1249.icry @@ -0,0 +1,12 @@ +// toSignedInteger + +toSignedInteger (0 : [64]) +:eval toSignedInteger (0 : [64]) +toSignedInteger (1 : [64]) +:eval toSignedInteger (1 : [64]) +toSignedInteger (2^^63 - 1 : [64]) +:eval toSignedInteger (2^^63 - 1 : [64]) +toSignedInteger (-1 : [64]) +:eval toSignedInteger (-1 : [64]) +toSignedInteger (-(2^^63) : [64]) +:eval toSignedInteger (-(2^^63) : [64]) diff --git a/tests/issues/issue1249.icry.stdout b/tests/issues/issue1249.icry.stdout new file mode 100644 index 000000000..562bc3d33 --- /dev/null +++ b/tests/issues/issue1249.icry.stdout @@ -0,0 +1,11 @@ +Loading module Cryptol +0 +0 +1 +1 +9223372036854775807 +9223372036854775807 +-1 +-1 +-9223372036854775808 +-9223372036854775808 From f8245edbf694072a1cb2c4039b6f6a667351f8aa Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 20 Dec 2024 09:19:51 -0600 Subject: [PATCH 2/2] Support deepseq in reference evaluator Checks off one box in #1249. --- CHANGES.md | 4 ++-- src/Cryptol/Eval/Reference.lhs | 30 +++++++++++++++++++++++++++++- tests/issues/issue1249.icry | 5 +++++ tests/issues/issue1249.icry.stdout | 7 +++++++ 4 files changed, 43 insertions(+), 3 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index ab73fa9a6..9e8ba0982 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -15,8 +15,8 @@ were incorrectly computed. ([#1773](https://github.com/GaloisInc/cryptol/issues/1773)) -* The reference evaluator now evaluates the `toSignedInteger` primitive instead - of panicking. +* The reference evaluator now evaluates the `toSignedInteger` and `deepseq` + primitives instead of panicking. ## New features diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 4ce7e99fb..d6eff26c7 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -247,7 +247,28 @@ Operations on Values > where > g (Nat n) = f n > g Inf = evalPanic "vFinPoly" ["Expected finite numeric type"] - +> +> -- | Reduce a value to normal form. +> forceValue :: Value -> E () +> forceValue v = +> case v of +> -- Values where the field is already is normal form +> VBit{} -> pure () +> VInteger{} -> pure () +> VRational{} -> pure () +> VFloat{} -> pure () +> -- Values with fields containing other values to reduce to normal form +> VList _ xs -> forceValues xs +> VTuple xs -> forceValues xs +> VRecord fs -> forceValues $ map snd fs +> VEnum _ xs -> forceValues xs +> -- Lambdas and other abstractions are already in normal form +> VFun{} -> pure () +> VPoly{} -> pure () +> VNumPoly{} -> pure () +> where +> forceValues :: [E Value] -> E () +> forceValues = mapM_ (\x -> forceValue =<< x) Environments ------------ @@ -948,6 +969,13 @@ by corresponding type classes: > -- executes parmap sequentially > pure $ VList n (map f' xs') > +> , "deepseq" ~> VPoly $ \_a -> pure $ +> VPoly $ \_b -> pure $ +> VFun $ \x -> pure $ +> VFun $ \y -> +> do forceValue =<< x +> y +> > , "error" ~> VPoly $ \_a -> pure $ > VNumPoly $ \_ -> pure $ > VFun $ \s -> diff --git a/tests/issues/issue1249.icry b/tests/issues/issue1249.icry index e89f65c3d..46d009c6d 100644 --- a/tests/issues/issue1249.icry +++ b/tests/issues/issue1249.icry @@ -10,3 +10,8 @@ toSignedInteger (-1 : [64]) :eval toSignedInteger (-1 : [64]) toSignedInteger (-(2^^63) : [64]) :eval toSignedInteger (-(2^^63) : [64]) + +// deepseq + +deepseq ((), undefined`{()}) True +:eval deepseq ((), undefined`{()}) True diff --git a/tests/issues/issue1249.icry.stdout b/tests/issues/issue1249.icry.stdout index 562bc3d33..4550eea81 100644 --- a/tests/issues/issue1249.icry.stdout +++ b/tests/issues/issue1249.icry.stdout @@ -9,3 +9,10 @@ Loading module Cryptol -1 -9223372036854775808 -9223372036854775808 + +Run-time error: undefined +-- Backtrace -- +Cryptol::error called at Cryptol:1062:13--1062:18 +Cryptol::undefined called at issue1249.icry:16:14--16:23 +Cryptol::deepseq called at issue1249.icry:16:1--16:8 +Run-time error: undefined