From ecf4765c4beab2656d57ba4982f42427a40bc016 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Wed, 28 Jun 2023 00:32:48 -0700
Subject: [PATCH] [ fix ] Fix issue with eager evaluation of crashing functions
 (fixes #3003) (#3004)

* [ fix ] Fix issue with eager evaluation of crashing functions

* Mark functions that call unsafe builtins as non-constant

* Better detection of crash primop when deciding if functions can be constant
---
 src/Compiler/Opts/ToplevelConstants.idr | 18 ++++++++++++++++--
 tests/Main.idr                          |  2 +-
 tests/chez/chez036/Crash.idr            | 14 ++++++++++++++
 tests/chez/chez036/Crash2.idr           | 15 +++++++++++++++
 tests/chez/chez036/Crash3.idr           |  9 +++++++++
 tests/chez/chez036/expected             |  2 ++
 tests/chez/chez036/run                  |  5 +++++
 7 files changed, 62 insertions(+), 3 deletions(-)
 create mode 100644 tests/chez/chez036/Crash.idr
 create mode 100644 tests/chez/chez036/Crash2.idr
 create mode 100644 tests/chez/chez036/Crash3.idr
 create mode 100644 tests/chez/chez036/expected
 create mode 100755 tests/chez/chez036/run

diff --git a/src/Compiler/Opts/ToplevelConstants.idr b/src/Compiler/Opts/ToplevelConstants.idr
index e7bf46cd65..dd16dd168f 100644
--- a/src/Compiler/Opts/ToplevelConstants.idr
+++ b/src/Compiler/Opts/ToplevelConstants.idr
@@ -15,7 +15,7 @@ import Libraries.Data.SortedMap
 --          Call Graph
 --------------------------------------------------------------------------------
 
--- direct calls from a top-level funtion's expression to other
+-- direct calls from a top-level function's expression to other
 -- top-level functions.
 0 CallGraph : Type
 CallGraph = SortedMap Name (SortedSet Name)
@@ -71,6 +71,7 @@ data SortTag : Type where
 record SortST where
   constructor SST
   processed : SortedSet Name
+  nonconst  : SortedSet Name
   triples   : SnocList (Name, FC, NamedDef)
   map       : SortedMap Name (Name, FC, NamedDef)
   graph     : CallGraph
@@ -94,6 +95,15 @@ markProcessed n = do
 isProcessed : Ref SortTag SortST => Name -> Core Bool
 isProcessed n = map (contains n . processed) (get SortTag)
 
+checkCrash : Ref SortTag SortST => (Name, FC, NamedDef) -> Core ()
+checkCrash (n, _, MkNmError _) = update SortTag $ { nonconst $= insert n }
+checkCrash (n, _, MkNmFun args (NmCrash _ _)) = update SortTag $ { nonconst $= insert n }
+checkCrash (n, _, MkNmFun args (NmOp _ Crash _)) = update SortTag $ { nonconst $= insert n }
+checkCrash (n, _, def) = do
+  st <- get SortTag
+  when (any (flip contains st.nonconst) !(getCalls n)) $
+    put SortTag $ { nonconst $= insert n } st
+
 sortDef : Ref SortTag SortST => Name -> Core ()
 sortDef n = do
   False  <- isProcessed n | True => pure ()
@@ -102,6 +112,7 @@ sortDef n = do
   traverse_ sortDef cs
   Just t <- getTriple n | Nothing => pure ()
   appendDef t
+  checkCrash t
 
 isConstant : (recursiveFunctions : SortedSet Name) -> (Name,FC,NamedDef) -> Bool
 isConstant rec (n, _, MkNmFun [] _) = not $ contains n rec
@@ -115,6 +126,7 @@ sortDefs ts =
       consts := map fst $ filter (isConstant rec) ts
       init   := SST {
                     processed = empty
+                  , nonconst  = empty
                   , triples   = Lin
                   , map       = fromList (map (\t => (fst t, t)) ts)
                   , graph     = graph
@@ -122,5 +134,7 @@ sortDefs ts =
    in do
      s       <- newRef SortTag init
      traverse_ sortDef (map fst ts)
-     sorted  <- map ((<>> []) . triples) (get SortTag)
+     st <- get SortTag
+     let sorted = triples st <>> []
+     let consts = filter (not . flip contains (nonconst st)) consts
      pure (sorted, fromList consts)
diff --git a/tests/Main.idr b/tests/Main.idr
index a95634ac62..9888cafcc5 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -308,7 +308,7 @@ chezTests = MkTestPool "Chez backend" [] (Just Chez)
     , "chez013", "chez014", "chez015", "chez016", "chez017", "chez018"
     , "chez019", "chez020", "chez021", "chez022", "chez023", "chez024"
     , "chez025", "chez026", "chez027", "chez028", "chez029", "chez030"
-    , "chez031", "chez032", "chez033", "chez034", "chez035"
+    , "chez031", "chez032", "chez033", "chez034", "chez035", "chez036"
     , "futures001"
     , "bitops"
     , "casts"
diff --git a/tests/chez/chez036/Crash.idr b/tests/chez/chez036/Crash.idr
new file mode 100644
index 0000000000..6f5c2d11a8
--- /dev/null
+++ b/tests/chez/chez036/Crash.idr
@@ -0,0 +1,14 @@
+-- no_clauses.idr
+%default total
+
+bad : (0 _ : Z = S Z) -> Void
+bad _ impossible
+
+data BadPrf = Ok | No (Z = S Z)
+
+Show BadPrf where
+    show Ok = "Ok"
+    show (No prf) = absurd $ bad prf
+
+main : IO ()
+main = printLn Ok
diff --git a/tests/chez/chez036/Crash2.idr b/tests/chez/chez036/Crash2.idr
new file mode 100644
index 0000000000..e42495f5ff
--- /dev/null
+++ b/tests/chez/chez036/Crash2.idr
@@ -0,0 +1,15 @@
+%noinline
+foo : (0 _ : Z = S Z) -> Void
+foo _ impossible
+
+%noinline
+bah : (0 _ : Z = S Z) -> Void
+bah prf = foo prf
+data BadPrf = Ok | No (Z = S Z)
+
+Show BadPrf where
+    show Ok = "Ok"
+    show (No prf) = absurd $ bah prf
+
+main : IO ()
+main = printLn Ok
diff --git a/tests/chez/chez036/Crash3.idr b/tests/chez/chez036/Crash3.idr
new file mode 100644
index 0000000000..40d8c92048
--- /dev/null
+++ b/tests/chez/chez036/Crash3.idr
@@ -0,0 +1,9 @@
+import System
+partial
+unreachable : a
+unreachable = idris_crash "unreachable"
+
+main : IO Int
+main = do
+    exitSuccess
+    assert_total unreachable
diff --git a/tests/chez/chez036/expected b/tests/chez/chez036/expected
new file mode 100644
index 0000000000..541dab48de
--- /dev/null
+++ b/tests/chez/chez036/expected
@@ -0,0 +1,2 @@
+Ok
+Ok
diff --git a/tests/chez/chez036/run b/tests/chez/chez036/run
new file mode 100755
index 0000000000..9dd6356087
--- /dev/null
+++ b/tests/chez/chez036/run
@@ -0,0 +1,5 @@
+$1 --no-banner --no-color --console-width 0 --exec main Crash.idr
+$1 --no-banner --no-color --console-width 0 --exec main Crash2.idr
+$1 --no-banner --no-color --console-width 0 --exec main Crash3.idr
+
+rm -rf build