From ffd47268feacb619b7bc0a998359b21fd38139b2 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Wed, 3 Nov 2021 08:01:36 -0400
Subject: [PATCH] Bring in support for ceil, floor, and atan2

This bumps the `crucible` submodule to bring in GaloisInc/crucible#905 and the
`copilot` submodule to bring in GaloisInc/copilot-1#3. Because this brings in
commit Copilot-Language/copilot@43e1efb95258b1555c55c1fef939082923116831, I had
to slightly adjust how `copilot-verifier` sets the output directory.

More progress towards GaloisInc/copilot-verifier#3.
---
 copilot-verifier/src/Copilot/Verifier.hs | 17 +++++++----------
 deps/copilot                             |  2 +-
 deps/crucible                            |  2 +-
 3 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/copilot-verifier/src/Copilot/Verifier.hs b/copilot-verifier/src/Copilot/Verifier.hs
index c7e7269..0cfa917 100644
--- a/copilot-verifier/src/Copilot/Verifier.hs
+++ b/copilot-verifier/src/Copilot/Verifier.hs
@@ -123,12 +123,6 @@ import What4.Solver.Adapter (SolverAdapter(..))
 import What4.Solver.Z3 (z3Adapter)
 import What4.Symbol (safeSymbol)
 
-setOutput :: CruxOptions -> CSettings -> CSettings
-setOutput cruxOpts cin =
-  case cSettingsOutputDirectory cin of
-    Nothing -> cin{ cSettingsOutputDirectory = Just (outDir cruxOpts)  }
-    Just _  -> cin
-
 verify :: CSettings -> [String] -> String -> Spec -> IO ()
 verify csettings0 properties prefix spec =
   do (cruxOpts, llvmOpts, csettings, csrc) <-
@@ -137,10 +131,13 @@ verify csettings0 properties prefix spec =
           -- TODO, load from and actual configuration file?
           fileOpts <- fromFile "copilot-verifier" cfg Nothing
           (cruxOpts0, llvmOpts0) <- foldM fromEnv fileOpts (cfgEnv cfg)
-          let odir = case cSettingsOutputDirectory csettings0 of
-                       Just d -> d
-                       Nothing -> "results" </> prefix
-          let csettings = csettings0{ cSettingsOutputDirectory = Just odir }
+          let odir0 = cSettingsOutputDirectory csettings0
+          let odir = -- A bit grimy, but this corresponds to how crux-llvm sets
+                     -- its output directory.
+                     if odir0 == "."
+                       then "results" </> prefix
+                       else odir0
+          let csettings = csettings0{ cSettingsOutputDirectory = odir }
           let csrc = odir </> prefix ++ ".c"
           let cruxOpts1 = cruxOpts0{ outDir = odir, bldDir = odir, inputFiles = [csrc] }
           ocfg <- defaultOutputConfig cruxLogMessageToSayWhat
diff --git a/deps/copilot b/deps/copilot
index 958ea0c..3172353 160000
--- a/deps/copilot
+++ b/deps/copilot
@@ -1 +1 @@
-Subproject commit 958ea0c86179a02958714891ab924447d6fc1f16
+Subproject commit 31723536f248c5f4ffd692bd53f411713df2d0ea
diff --git a/deps/crucible b/deps/crucible
index ffa247c..be045ac 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit ffa247c549e42ff3325eb8f03fd2eacfc8480a14
+Subproject commit be045ac04850e318aba38541bbc6dae5844d49c3