Skip to content

Commit

Permalink
Support toSignedInteger in reference evaluator
Browse files Browse the repository at this point in the history
Checks off one box in #1249.
  • Loading branch information
RyanGlScott committed Dec 20, 2024
1 parent 9cb3eed commit 6bd8c5e
Show file tree
Hide file tree
Showing 4 changed files with 30 additions and 0 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 <FILE> <EXPR>` updated to write to stdout when
Expand Down
4 changes: 4 additions & 0 deletions src/Cryptol/Eval/Reference.lhs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
12 changes: 12 additions & 0 deletions tests/issues/issue1249.icry
Original file line number Diff line number Diff line change
@@ -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])
11 changes: 11 additions & 0 deletions tests/issues/issue1249.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
Loading module Cryptol
0
0
1
1
9223372036854775807
9223372036854775807
-1
-1
-9223372036854775808
-9223372036854775808

0 comments on commit 6bd8c5e

Please sign in to comment.