Merge remote-tracking branch 'upstream/master' into partllvmval-rebased

README.md

@@ -46,13 +46,13 @@ Currently, the repository consists of the following Haskell packages:
    and verification.  This includes most of the setup steps required
    to actually set the simulator off and running, as well as
    functionality for collecting and discharging safety conditions and
-   generated assertions via solvers.  Both the `crucible-c` and `crucible-jvm`
+   generated assertions via solvers.  Both the `crux-llvm` and `crucible-jvm`
    executables are thin wrappers around the functionality provided
    by `crux`.
 
 In addition, there are the following library/executable packages:
 
- * **`crucible-c`**, a standalone frontend for executing C programs
+ * **`crux-llvm`**, a standalone frontend for executing C and C++ programs
    in the crucible symbolic simulator.  The front-end invokes `clang`
    to produce LLVM bitcode, and runs the resulting programs using
    the `crucible-llvm` language frontend.  Programs interact directly
@@ -63,7 +63,7 @@ In addition, there are the following library/executable packages:
 
  * **`crucible-jvm`**, also contains an executable for directly
    running compiled JVM bytecode programs, in a similar vein
-   to the `crucible-c` package.
+   to the `crux-llvm` package.
 
  * **`crucible-server`**, a standalone process that allows constructing
    and symbolically executing Crucible programs via [Protocol Buffers][pb].

cabal.project

@@ -10,13 +10,13 @@ packages:
   what4-blt/
 
   crucible/
-  crucible-c/
   crucible-jvm/
   crucible-llvm/
   crucible-saw/
   crucible-server/
   crucible-syntax/
   crux/
+  crux-llvm/
 
 optional-packages:
   dependencies/abcBridge/

crucible-llvm/crucible-llvm.cabal

@@ -25,6 +25,7 @@ library
     hashable,
     hashtables,
     lens,
+    itanium-abi,
     llvm-pretty >= 0.8 && < 0.11,
     mtl,
     parameterized-utils >= 1.0.4 && < 1.1,
@@ -42,6 +43,7 @@ library
     Lang.Crucible.LLVM.Arch.Util
     Lang.Crucible.LLVM.Arch.X86
     Lang.Crucible.LLVM.Bytes
+    Lang.Crucible.LLVM.Ctors
     Lang.Crucible.LLVM.DataLayout
     Lang.Crucible.LLVM.Extension
     Lang.Crucible.LLVM.Extension.Safety
@@ -57,9 +59,15 @@ library
     Lang.Crucible.LLVM.TypeContext
 
   other-modules:
+<<<<<<< HEAD
     Lang.Crucible.LLVM.Extension.Arch
     Lang.Crucible.LLVM.Extension.Syntax
     Lang.Crucible.LLVM.Extension.Safety.Standards
+=======
+    Lang.Crucible.LLVM.Intrinsics.Common
+    Lang.Crucible.LLVM.Intrinsics.Libc
+    Lang.Crucible.LLVM.Intrinsics.Libcxx
+>>>>>>> upstream/master
     Lang.Crucible.LLVM.MemModel.Common
     Lang.Crucible.LLVM.MemModel.Generic
     Lang.Crucible.LLVM.MemModel.Partial

crucible-llvm/src/Lang/Crucible/LLVM.hs

@@ -20,29 +20,32 @@ module Lang.Crucible.LLVM
 where
 
 import           Control.Lens
+import           Control.Monad (when)
+import           Data.Maybe (isJust)
 import qualified Text.LLVM.AST as L
 
 import           Lang.Crucible.Analysis.Postdom
-import           Lang.Crucible.CFG.Core
-import           Lang.Crucible.FunctionHandle
-import           Lang.Crucible.LLVM.Arch
-import           Lang.Crucible.LLVM.Extension
+import           Lang.Crucible.CFG.Core (AnyCFG(..), cfgHandle)
+import           Lang.Crucible.FunctionHandle (lookupHandleMap, handleName)
+import           Lang.Crucible.LLVM.Arch (llvmExtensionEval)
+import           Lang.Crucible.LLVM.Extension (LLVM, ArchWidth)
 import           Lang.Crucible.LLVM.Intrinsics
 import           Lang.Crucible.LLVM.MemModel
 import           Lang.Crucible.Simulator.ExecutionTree
 import           Lang.Crucible.Simulator.GlobalState
-import           Lang.Crucible.Simulator.OverrideSim
-
-
+import           Lang.Crucible.Simulator.OverrideSim (OverrideSim, bindFnHandle)
+import           Lang.Crucible.Utils.MonadVerbosity (showWarning)
 
 registerModuleFn
    :: (L.Symbol, AnyCFG (LLVM arch))
    -> OverrideSim p sym (LLVM arch) rtp l a ()
 registerModuleFn (_,AnyCFG cfg) = do
   let h = cfgHandle cfg
       s = UseCFG cfg (postdomInfo cfg)
-  stateContext . functionBindings %= insertHandleMap h s
-
+  binds <- use (stateContext . functionBindings)
+  when (isJust $ lookupHandleMap h binds) $
+    showWarning ("LLVM function handle registered twice: " ++ show (handleName h))
+  bindFnHandle h s
 
 llvmGlobals
    :: LLVMContext arch