diff --git a/CHANGES.md b/CHANGES.md index 11ffd01cd..9e8ba0982 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` and `deepseq` + primitives 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..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 ------------ @@ -758,6 +779,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 -> @@ -944,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 new file mode 100644 index 000000000..46d009c6d --- /dev/null +++ b/tests/issues/issue1249.icry @@ -0,0 +1,17 @@ +// 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]) + +// deepseq + +deepseq ((), undefined`{()}) True +:eval deepseq ((), undefined`{()}) True diff --git a/tests/issues/issue1249.icry.stdout b/tests/issues/issue1249.icry.stdout new file mode 100644 index 000000000..4550eea81 --- /dev/null +++ b/tests/issues/issue1249.icry.stdout @@ -0,0 +1,18 @@ +Loading module Cryptol +0 +0 +1 +1 +9223372036854775807 +9223372036854775807 +-1 +-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