Getting `Prelude.tail: empty list` error when running crucible-llvm with profiling in split-dfs path mode

[Lukas-Dresel]

Reproduce on a Mac with the attached files:

cabal run exe:crux-llvm -- -O0 --profile-crucible --path-strategy=split-dfs ../bug_prelude.tail/stbi_read_crucible_harness.c

When debugging this with @RyanGlScott we narrowed it down to likely being the tail call in Simulator/Profiling.hs in openEventFrames being called on an empty list.

See https://github.com/GaloisInc/crucible/blob/4158b6f696c0c88fd6b1b698ffea7aad8bee8597/crucible/src/Lang/Crucible/Simulator/Profiling.hs#L293

bug_prelude.tail.tar.gz

[Lukas-Dresel]

Fun fact, removing the -O0 causes LLVM to crash instead

[RyanGlScott]

Here is a simpler way to trigger the crash:

#include <stdint.h>
#include "crucible.h"

int main() {
  if (crucible_int8_t("x")) {
    return 1;
  } else {
    return 0;
  }
}

$ ~/Software/crux-llvm-0.6/bin/crux-llvm -O0 --profile-crucible --path-strategy=split-dfs test.c
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] Total paths explored: 2
Prelude.tail: empty list

Removing -O0 on this example doesn't cause LLVM to crash, thankfully enough, but it does make the bug disappear.

[RyanGlScott]

If you add some Debug.Trace'ing to openEventFrames, the function responsible for calling tail:

diff --git a/crucible/src/Lang/Crucible/Simulator/Profiling.hs b/crucible/src/Lang/Crucible/Simulator/Profiling.hs
index 14b74a16..79a8aeb7 100644
--- a/crucible/src/Lang/Crucible/Simulator/Profiling.hs
+++ b/crucible/src/Lang/Crucible/Simulator/Profiling.hs
@@ -81,6 +81,7 @@ import           Lang.Crucible.Simulator.EvalStmt
 import           Lang.Crucible.Simulator.ExecutionTree
 import           Lang.Crucible.Simulator.Operations

+import Debug.Trace

 data Metrics f =
   Metrics
@@ -283,7 +284,7 @@ readProfilingState tbl =
      return (now, toList cgevs ++ closingEvents now m cgevs, toList sevs)

 openEventFrames :: Seq CGEvent -> [CGEvent]
-openEventFrames = go []
+openEventFrames y = go [] $ trace (show (fmap cgEvent_type y)) y
  where
  go :: [CGEvent] -> Seq CGEvent -> [CGEvent]
  go xs Seq.Empty = xs

You'll get this on the program above:

fromList [ENTER,ENTER,ENTER,ENTER,EXIT,EXIT,EXIT,ENTER,EXIT,EXIT,EXIT,ENTER,EXIT,EXIT]

Note that there are more EXITs (8) than ENTERs (6), which is likely confusing the bookkeeping code in openEventFrames.

[robdockins]

As a first step, we should obviously remove the use of tail and replace it with pattern matching and a call to panic or similar.

After that, we should figure out why the profiling bookeeping is going wrong.