Sygus2

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

@@ -43,7 +43,6 @@ import           Data.Parameterized.Context ( pattern (:>), pattern Empty )
 import qualified Data.Parameterized.Context as Ctx
 
 import           What4.Interface
-import           What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder(..))
 import           What4.ProgramLoc (plSourceLoc)
 import qualified What4.SpecialFunctions as W4
 

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

@@ -790,9 +790,10 @@ readMem' sym w end gsym l0 origMem tp0 alignment (MemWrites ws) =
         else do -- We're playing a trick here.  By making a fresh constant a proof obligation, we can be
                 -- sure it always fails.  But, because it's a variable, it won't be constant-folded away
                 -- and we can be relatively sure the annotation will survive.
-                b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr
-                Partial.Err <$>
-                  Partial.annotateME sym mop (NoSatisfyingWrite tp) b
+                -- b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr
+                -- Partial.Err <$>
+                --   Partial.annotateME sym mop (NoSatisfyingWrite tp) b
+                Partial.partErr sym mop (NoSatisfyingWrite tp)
 
     go :: (StorageType -> LLVMPtr sym w -> ReadMem sym (PartLLVMVal sym)) ->
           LLVMPtr sym w ->

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

@@ -68,6 +68,7 @@ module Lang.Crucible.LLVM.MemModel.MemLog
 
     -- * Write ranges
   , writeRangesMem
+  , writeSourceSize
 
     -- * Concretization
   , concPtr

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

@@ -95,6 +95,12 @@ module Lang.Crucible.LLVM.SimpleLoopInvariant
   ( InvariantEntry(..)
   , InvariantPhase(..)
   , simpleLoopInvariant
+  -- , MemorySubstitution(..)
+  -- , computeMemSubstitution
+  -- , constructMemSubstitutionCandidate
+  -- , checkMemSubst
+  -- , loadMemJoinVariables
+  -- , storeMemJoinVariables
   ) where
 
 import           Control.Lens

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

@@ -101,7 +101,6 @@ import           Lang.Crucible.LLVM.TypeContext
 import           Lang.Crucible.Syntax
 import           Lang.Crucible.Types
 
-import           What4.InterpretedFloatingPoint (X86_80Val(..))
 
 -------------------------------------------------------------------------
 -- LLVMExpr

crucible/src/Lang/Crucible/Analysis/Fixpoint/Components.hs

@@ -21,6 +21,7 @@ module Lang.Crucible.Analysis.Fixpoint.Components (
   weakTopologicalOrdering,
   WTOComponent(..),
   SCC(..),
+  parentWTOComponent,
   -- * Special cases
   cfgWeakTopologicalOrdering,
   cfgSuccessors,
@@ -239,6 +240,23 @@ unlabeled = Label 0
 maxLabel :: Label
 maxLabel = Label maxBound
 
+-- | Construct a map from each vertex to the head of its parent WTO component.
+-- In particular, the head of a component is mapped to itself. The top vertices
+-- are not in the map.
+parentWTOComponent :: (Ord n) => [WTOComponent n] -> M.Map n n
+parentWTOComponent = F.foldMap' $ \case
+  SCC scc' -> parentWTOComponent' scc'
+  Vertex{} -> M.empty
+
+parentWTOComponent' :: (Ord n) => SCC n -> M.Map n n
+parentWTOComponent' scc = -- M.singleton (wtoHead scc) (wtoHead scc) <>
+  F.foldMap'
+    (\case
+      SCC scc' -> parentWTOComponent' scc'
+      Vertex v -> M.singleton v $ wtoHead scc)
+    (wtoComps scc)
+
+
 {- Note [Bourdoncle Components]
 
 Bourdoncle components are a weak topological ordering of graph

crucible/src/Lang/Crucible/Backend.hs

@@ -95,6 +95,11 @@ module Lang.Crucible.Backend
   , addFailedAssertion
   , assertIsInteger
   , readPartExpr
+  , runCHC
+  , proofObligationsAsImplications
+  , convertProofObligationsAsImplications
+  , proofObligationsUninterpConstants
+  , pathConditionUninterpConstants
   , ppProofObligation
   , backendOptions
   , assertThenAssumeConfigOption
@@ -110,17 +115,25 @@ import           Data.Functor.Identity
 import           Data.Functor.Const
 import qualified Data.Sequence as Seq
 import           Data.Sequence (Seq)
+import           Data.Set (Set)
 import qualified Prettyprinter as PP
 import           GHC.Stack
+import           System.IO
+
+import           Data.Parameterized.Map (MapF)
 
 import           What4.Concrete
 import           What4.Config
+import           What4.Expr.Builder
 import           What4.Interface
 import           What4.InterpretedFloatingPoint
 import           What4.LabeledPred
 import           What4.Partial
 import           What4.ProgramLoc
 import           What4.Expr (GroundValue, GroundValueWrapper(..))
+import           What4.Solver
+import qualified What4.Solver.CVC5 as CVC5
+import qualified What4.Solver.Z3 as Z3
 
 import qualified Lang.Crucible.Backend.AssumptionStack as AS
 import qualified Lang.Crucible.Backend.ProofGoals as PG
@@ -613,6 +626,68 @@ readPartExpr bak (PE p v) msg = do
   addAssertion bak (LabeledPred p (SimError loc msg))
   return v
 
+
+-- | Run the CHC solver on the current proof obligations, and return the
+-- solution as a substitution from the uninterpreted functions to their
+-- definitions.
+runCHC ::
+  (IsSymBackend sym bak, sym ~ ExprBuilder t st fs, MonadIO m) =>
+  bak ->
+  [SomeSymFn sym] ->
+  m (MapF (SymFnWrapper sym) (SymFnWrapper sym))
+runCHC bak uninterp_inv_fns  = liftIO $ do
+  let sym = backendGetSym bak
+
+  implications <- proofObligationsAsImplications bak
+  clearProofObligations bak
+
+  withFile "foo.smt2" WriteMode $ \handle ->
+    Z3.writeZ3HornSMT2File sym True handle uninterp_inv_fns implications
+  withFile "foo.sy" WriteMode $ \handle ->
+    CVC5.writeCVC5SyFile sym handle uninterp_inv_fns implications
+
+  -- log to stdout
+  let logData = defaultLogData
+        { logCallbackVerbose = \_ -> putStrLn
+        , logReason = "SAW inv"
+        }
+  Z3.runZ3Horn sym True logData uninterp_inv_fns implications >>= \case
+    Sat sub -> return sub
+    Unsat{} -> fail "Prover returned Infeasible"
+    Unknown -> fail "Prover returned Fail"
+  -- CVC5.runCVC5SyGuS sym logData uninterp_inv_fns implications >>= \case
+  --   Sat sub -> return sub
+  --   Unsat{} -> fail "Prover returned Infeasible"
+  --   Unknown -> fail "Prover returned Fail"
+
+
+-- | Get proof obligations as What4 implications.
+proofObligationsAsImplications :: IsSymBackend sym bak => bak -> IO [Pred sym]
+proofObligationsAsImplications bak = do
+  let sym = backendGetSym bak
+  convertProofObligationsAsImplications sym =<< getProofObligations bak
+
+-- | Convert proof obligations to What4 implications.
+convertProofObligationsAsImplications :: IsSymInterface sym => sym -> ProofObligations sym -> IO [Pred sym]
+convertProofObligationsAsImplications sym goals = do
+  let obligations = maybe [] PG.goalsToList goals
+  forM obligations $ \(AS.ProofGoal hyps (LabeledPred concl _err)) -> do
+    hyp <- assumptionsPred sym hyps
+    impliesPred sym hyp concl
+
+-- | Get the set of uninterpreted constants that appear in the path condition.
+pathConditionUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym)))
+pathConditionUninterpConstants bak = do
+  let sym = backendGetSym bak
+  exprUninterpConstants sym <$> getPathCondition bak
+
+-- | Get the set of uninterpreted constants that appear in the proof obligations.
+proofObligationsUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym)))
+proofObligationsUninterpConstants bak = do
+  let sym = backendGetSym bak
+  foldMap (exprUninterpConstants sym) <$> proofObligationsAsImplications bak
+
+
 ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (PP.Doc ann)
 ppProofObligation sym (AS.ProofGoal asmps gl) =
   do as <- flattenAssumptions sym asmps

crucible/src/Lang/Crucible/Backend/ProofGoals.hs

@@ -166,7 +166,7 @@ traverseGoalsWithAssumptions f gls =
 --   primarily a debugging aid, to ensure that stack management
 --   remains well-bracketed.
 newtype FrameIdentifier = FrameIdentifier Word64
- deriving(Eq,Ord)
+ deriving(Eq,Ord,Show)
 
 
 -- | A data-strucutre that can incrementally collect goals in context.

crucible/src/Lang/Crucible/CFG/Expr.hs

@@ -75,7 +75,6 @@ import qualified Data.Parameterized.TH.GADT as U
 import           Data.Parameterized.TraversableFC
 
 import           What4.Interface (RoundingMode(..),StringLiteral(..), stringLiteralInfo)
-import           What4.InterpretedFloatingPoint (X86_80Val(..))
 
 import           Lang.Crucible.CFG.Extension
 import           Lang.Crucible.FunctionHandle

crucible/src/Lang/Crucible/FunctionHandle.hs

@@ -34,6 +34,7 @@ module Lang.Crucible.FunctionHandle
   , emptyHandleMap
   , insertHandleMap
   , lookupHandleMap
+  , updateHandleMap
   , searchHandleMap
   , handleMapToHandles
     -- * Reference cells
@@ -44,6 +45,7 @@ module Lang.Crucible.FunctionHandle
 
 import           Data.Hashable
 import           Data.Kind
+import           Data.Functor.Identity
 import qualified Data.List as List
 import           Data.Ord (comparing)
 
@@ -217,6 +219,19 @@ lookupHandleMap hdl (FnHandleMap m) =
      Just (HandleElt _ x) -> Just x
      Nothing -> Nothing
 
+-- | Update the entry of the function handle in the map.
+updateHandleMap :: (f args ret -> f args ret)
+                -> FnHandle args ret
+                -> FnHandleMap f
+                -> FnHandleMap f
+updateHandleMap f hdl (FnHandleMap m) =
+  FnHandleMap $ MapF.updatedValue $ runIdentity $
+    MapF.updateAtKey
+      (handleID hdl)
+      (Identity Nothing)
+      (\(HandleElt hdl' x) -> Identity $ MapF.Set $ HandleElt hdl' $ f x)
+      m
+
 -- | Lookup the function name in the map by a linear scan of all
 -- entries.  This will be much slower than using 'lookupHandleMap' to
 -- find the function by ID, so the latter should be used if possible.

crucible/src/Lang/Crucible/Simulator/EvalStmt.hs

@@ -60,7 +60,6 @@ import           Prettyprinter
 
 import           What4.Config
 import           What4.Interface
-import           What4.InterpretedFloatingPoint (freshFloatConstant)
 import           What4.Partial
 import           What4.ProgramLoc
 

crucible/src/Lang/Crucible/Types.hs

@@ -95,16 +95,7 @@ module Lang.Crucible.Types
   , module Data.Parameterized.NatRepr
   , module Data.Parameterized.SymbolRepr
   , module What4.BaseTypes
-  , FloatInfo
-  , HalfFloat
-  , SingleFloat
-  , DoubleFloat
-  , QuadFloat
-  , X86_80Float
-  , DoubleDoubleFloat
-  , FloatInfoRepr(..)
-  , FloatInfoToBitWidth
-  , floatInfoToBVTypeRepr
+  , module What4.InterpretedFloatingPoint
   ) where
 
 import           Data.Hashable