Skip to content

Commit

Permalink
Abort early after type-checking malformed constraint guards
Browse files Browse the repository at this point in the history
Checking ill-typed constraint guards for exhaustivity can cause Cryptol to
panic. If we detect any type errors after type-checking the guards, we now
abort early and report any recorded errors instead of proceeding to check
exhaustivity.

Fixes #1593. Fixes #1693.
  • Loading branch information
RyanGlScott committed Jul 2, 2024
1 parent a483c1e commit 6e417aa
Show file tree
Hide file tree
Showing 8 changed files with 39 additions and 0 deletions.
4 changes: 4 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,10 @@

* Fix #1685, which caused Cryptol to panic when given a local definition without
a type signature that uses numeric constraint guards.

* Fix #1593 and #1693, two related bugs that would cause Cryptol to panic when
checking ill-typed constraint guards for exhaustivity.

# 3.1.0 -- 2024-02-05

## Language changes
Expand Down
5 changes: 5 additions & 0 deletions src/Cryptol/TypeCheck/Infer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1234,6 +1234,11 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
asmps1 <- applySubstPreds asmps0
t1 <- applySubst t0
cases1 <- mapM (checkPropGuardCase asmps1) cases0
-- If we recorded any errors when type-checking the constraint guards,
-- then abort early. We don't want to check exhaustivity if there are
-- malformed constraints, as these can cause panics elsewhere during
-- exhaustivity checking (see the `issue{1593,1693}` test cases).
abortIfErrors

exh <- checkExhaustive (P.bName b) as asmps1 (map fst cases1)
unless exh $
Expand Down
5 changes: 5 additions & 0 deletions tests/issues/issue1593.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
f : {n, a} [n]a -> [8]
f x
| n == 1 => 0
| n != 1 => 1
| Eq a => 2 // Malformed
1 change: 1 addition & 0 deletions tests/issues/issue1593.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
:load issue1593.cry
7 changes: 7 additions & 0 deletions tests/issues/issue1593.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main

[error] at issue1593.cry:5:5--5:9:
`Eq` may not be used in a constraint guard.
Constraint guards support only numeric comparisons and `fin`.
4 changes: 4 additions & 0 deletions tests/issues/issue1693.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
f : {n} [n] -> [n+1]
f x
| (fin n) => x # [False]
| (inf n) => x
1 change: 1 addition & 0 deletions tests/issues/issue1693.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
:load issue1693.cry
12 changes: 12 additions & 0 deletions tests/issues/issue1693.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main

[error] at issue1693.cry:1:5--1:21:
Incorrect type form.
Expected: a constraint
Inferred: a numeric type
[error] at issue1693.cry:4:5--4:12:
Incorrect type form.
Expected: a constraint
Inferred: a numeric type

0 comments on commit 6e417aa

Please sign in to comment.