Merge pull request #2474 from GaloisInc/bh/variable

saw-core: Rename 'ExtCns' term constructor to 'Variable'.

Author: brianhuffman

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -46,7 +46,7 @@ import Lang.Crucible.Simulator
 import Lang.Crucible.Types
 
 import qualified SAWCore.Prelude as SAW
-import qualified SAWCore.Recognizer as SAW (asExtCns)
+import qualified SAWCore.Recognizer as SAW (asVariable)
 import qualified SAWCore.SharedTerm as SAW
 import qualified SAWCoreWhat4.ReturnTrip as SAW
 import qualified CryptolSAWCore.TypedTerm as SAW
@@ -399,7 +399,7 @@ gatherAsserts msb =
         gatherSubsts postOnlyVars vars [] [] asserts'
     substTerms <- forM substs $ \(Pair var expr) -> do
         varTerm <- liftIO $ eval $ W4.BoundVarExpr var
-        varEc <- case SAW.asExtCns varTerm of
+        varEc <- case SAW.asVariable varTerm of
             Just ec -> return ec
             Nothing -> error $ "eval of BoundVarExpr produced non-ExtCns ?" ++ show varTerm
         exprTerm <- liftIO $ eval expr

crucible-mir-comp/src/Mir/Compositional/Convert.hs

@@ -330,7 +330,7 @@ exprToTerm sym sc w4VarMapRef val = liftIO $ do
     ty <- SAW.baseSCType sym sc (W4.exprType val)
     ec <- SAW.scFreshEC sc "w4expr" ty
     modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some val)
-    term <- SAW.scExtCns sc ec
+    term <- SAW.scVariable sc ec
     return term
 
 regToTerm :: forall sym t st fs tp0 m.

crucible-mir-comp/src/Mir/Compositional/Override.hs

@@ -365,7 +365,7 @@ matchArg sym sc eval allocSpecs md shp0 rv0 sv0 = go shp0 rv0 sv0
     go (PrimShape _ _btpr) expr (MS.SetupTerm tt) = do
         loc <- use MS.osLocation
         exprTerm <- liftIO $ eval expr
-        case SAW.asExtCns $ SAW.ttTerm tt of
+        case SAW.asVariable $ SAW.ttTerm tt of
             Just ec -> do
                 let var = SAW.ecVarIndex ec
                 sub <- use MS.termSub

crux-mir-comp/src/Mir/Cryptol.hs

@@ -58,7 +58,7 @@ import qualified CryptolSAWCore.Prelude as SAW
 import qualified CryptolSAWCore.CryptolEnv as SAW
 import qualified SAWCore.SharedTerm as SAW
 import qualified SAWCoreWhat4.ReturnTrip as SAW
-import qualified SAWCore.Recognizer as SAW (asExtCns)
+import qualified SAWCore.Recognizer as SAW (asVariable)
 import qualified CryptolSAWCore.TypedTerm as SAW
 
 import SAWCentral.Crucible.MIR.TypeShape
@@ -303,7 +303,7 @@ munge sym shp0 rv0 = do
             visitExprVars visitCache x $ \var -> do
                 let expr = W4.BoundVarExpr var
                 term <- eval' expr
-                ec <- case SAW.asExtCns term of
+                ec <- case SAW.asVariable term of
                     Just ec -> return ec
                     Nothing -> error "eval on BoundVarExpr produced non-ExtCns?"
                 modifyIORef w4VarMapRef $ Map.insert (SAW.ecVarIndex ec) (Some expr)

cryptol-saw-core/src/CryptolSAWCore/Monadify.hs

@@ -173,7 +173,7 @@ asTypedGlobalDef t =
     Constant nm ->
       let ty = resolvedNameType (requireNameInMap nm ?mm)
       in Just $ GlobalDef (nameInfo nm) (nameIndex nm) ty t
-    FTermF (ExtCns ec) ->
+    FTermF (Variable ec) ->
       Just $ GlobalDef (ecName ec) (ecVarIndex ec) (ecType ec) t
     _ -> Nothing
 

cryptol-saw-core/src/CryptolSAWCore/TypedTerm.hs

@@ -29,7 +29,7 @@ import qualified SAWSupport.Pretty as PPS (defaultOpts)
 
 import CryptolSAWCore.Cryptol (scCryptolType, Env, importKind, importSchema)
 import SAWCore.FiniteValue
-import SAWCore.Recognizer (asExtCns)
+import SAWCore.Recognizer (asVariable)
 import SAWCore.SharedTerm
 import SAWCore.SCTypeCheck (scTypeCheckError)
 import SAWCore.Term.Pretty (ppTerm)
@@ -189,7 +189,7 @@ typedTermOfFirstOrderValue sc fov =
      t <- scFirstOrderValue sc fov
      pure $ TypedTerm (TypedTermSchema (C.tMono cty)) t
 
--- Typed external constants ----------------------------------------------------
+-- Typed named variables -------------------------------------------------------
 
 data TypedExtCns =
   TypedExtCns
@@ -198,17 +198,17 @@ data TypedExtCns =
   }
   deriving Show
 
--- | Recognize 'TypedTerm's that are external constants.
+-- | Recognize 'TypedTerm's that are named variables.
 asTypedExtCns :: TypedTerm -> Maybe TypedExtCns
 asTypedExtCns (TypedTerm tp t) =
   do cty <- ttIsMono tp
-     ec <- asExtCns t
+     ec <- asVariable t
      pure $ TypedExtCns cty ec
 
 -- | Make a 'TypedTerm' from a 'TypedExtCns'.
 typedTermOfExtCns :: SharedContext -> TypedExtCns -> IO TypedTerm
 typedTermOfExtCns sc (TypedExtCns cty ec) =
-  TypedTerm (TypedTermSchema (C.tMono cty)) <$> scExtCns sc ec
+  TypedTerm (TypedTermSchema (C.tMono cty)) <$> scVariable sc ec
 
 abstractTypedExts :: SharedContext -> [TypedExtCns] -> TypedTerm -> IO TypedTerm
 abstractTypedExts sc tecs (TypedTerm (TypedTermSchema (C.Forall params props ty)) trm) =

saw-central/src/SAWCentral/Builtins.hs

@@ -758,7 +758,7 @@ extract_uninterp unints opaques tt =
      let tt' = tt{ ttTerm = tm }
 
      let f = traverse $ \(ec,vs) ->
-               do ectm <- scExtCns sc ec
+               do ectm <- scVariable sc ec
                   vs'  <- filterCryTerms sc vs
                   pure (ectm, vs')
      repls' <- io (traverse f repls)
@@ -779,7 +779,7 @@ extract_uninterp unints opaques tt =
      unless (Set.null boundAndUsed)
        (do ppOpts <- getTopLevelPPOpts
            vs <- io $ forM (Set.toList boundAndUsed) $ \ec ->
-                              do pptm <- scPrettyTerm ppOpts <$> scExtCns sc ec
+                              do pptm <- scPrettyTerm ppOpts <$> scVariable sc ec
                                  let ppty = scPrettyTerm ppOpts (ecType ec)
                                  return (pptm <> " : " <> ppty)
            printOutLnTop Warn $ unlines $
@@ -827,17 +827,17 @@ build_congruence sc tm =
        fail "congruence_for: cannot build congruence for dependent functions"
 
   loop [] vars =
-    do lvars <- mapM (scExtCns sc . fst) (reverse vars)
-       rvars <- mapM (scExtCns sc . snd) (reverse vars)
+    do lvars <- mapM (scVariable sc . fst) (reverse vars)
+       rvars <- mapM (scVariable sc . snd) (reverse vars)
        let allVars = concat [ [l,r] | (l,r) <- reverse vars ]
 
        basel <- scApplyAll sc tm lvars
        baser <- scApplyAll sc tm rvars
        baseeq <- scEqTrue sc =<< scEq sc basel baser
 
        let f x (l,r) =
-             do l' <- scExtCns sc l
-                r' <- scExtCns sc r
+             do l' <- scVariable sc l
+                r' <- scVariable sc r
                 eq <- scEqTrue sc =<< scEq sc l' r'
                 scFun sc eq x
        finalEq <- foldM f baseeq vars
@@ -1345,7 +1345,7 @@ proveByBVInduction script t =
          do wt  <- io $ scNat sc w
             natty <- io $ scNatType sc
             toNat <- io $ scGlobalDef sc "Prelude.bvToNat"
-            vars  <- io $ mapM (scExtCns sc) pis
+            vars  <- io $ mapM (scVariable sc) pis
             innerVars <-
               io $ sequence $
               [ scFreshGlobal sc ("i_" <> toShortName (ecName ec)) (ecType ec) | ec <- pis ]

saw-central/src/SAWCentral/Crucible/Common/Override.hs

@@ -552,7 +552,7 @@ refreshTerms sc ss =
   where
     freshenTerm (TypedExtCns _cty ec) =
       do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec)
-         new <- liftIO $ scExtCns sc ec'
+         new <- liftIO $ scVariable sc ec'
          return (ecVarIndex ec, new)
 
 -- | An override packaged together with its preconditions, labeled with some
@@ -723,7 +723,7 @@ matchTerm sc md prepost real expect =
   do let loc = MS.conditionLoc md
      free <- OM (use osFree)
      case unwrapTermF expect of
-       FTermF (ExtCns ec)
+       FTermF (Variable ec)
          | Set.member (ecVarIndex ec) free ->
          do assignTerm sc md prepost (ecVarIndex ec) real
 

saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs

@@ -790,7 +790,7 @@ verifyPoststate cc mspec env0 globals ret mdMap =
            [ (ecVarIndex ec, ec)
            | tt <- mspec ^. MS.csPreState . MS.csFreshVars
            , let ec = tecExt tt ]
-     terms0 <- io $ traverse (scExtCns sc) ecs0
+     terms0 <- io $ traverse (scVariable sc) ecs0
 
      let initialFree = Set.fromList (map (ecVarIndex . tecExt)
                                     (view (MS.csPostState . MS.csFreshVars) mspec))

saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs

@@ -394,12 +394,12 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
      lemmas' <- checkModuleCompatibility lm lemmas
      withMethodSpec checkSat lm nm setup $ \cc method_spec ->
        do let value_input_parameters = mapMaybe
-                (\(_, setup_value) -> setupValueAsExtCns setup_value)
+                (\(_, setup_value) -> setupValueAsVariable setup_value)
                 (Map.elems $ method_spec ^. MS.csArgBindings)
           let reference_input_parameters = mapMaybe
                 (\case
-                  LLVMPointsTo _ _ _ setup_value -> llvmPointsToValueAsExtCns setup_value
-                  LLVMPointsToBitfield _ _ _ val -> setupValueAsExtCns val)
+                  LLVMPointsTo _ _ _ setup_value -> llvmPointsToValueAsVariable setup_value
+                  LLVMPointsToBitfield _ _ _ val -> setupValueAsVariable val)
                 (method_spec ^. MS.csPreState ^. MS.csPointsTos)
           let input_parameters = nub $ value_input_parameters ++ reference_input_parameters
           let pre_free_variables = Map.fromList $
@@ -416,13 +416,13 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
 
           let return_output_parameter =
                 case method_spec ^. MS.csRetValue of
-                  Just setup_value -> setupValueAsExtCns setup_value
+                  Just setup_value -> setupValueAsVariable setup_value
                   Nothing -> Nothing
           let reference_output_parameters =
                 mapMaybe
                 (\case
-                  LLVMPointsTo _ _ _ setup_value -> llvmPointsToValueAsExtCns setup_value
-                  LLVMPointsToBitfield _ _ _ val -> setupValueAsExtCns val)
+                  LLVMPointsTo _ _ _ setup_value -> llvmPointsToValueAsVariable setup_value
+                  LLVMPointsToBitfield _ _ _ val -> setupValueAsVariable val)
                 (method_spec ^. MS.csPostState ^. MS.csPointsTos)
           let output_parameters =
                 nub $ filter (isNothing . (Map.!?) pre_free_variables) $
@@ -458,7 +458,7 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
           extracted_func_const <-
             io $ scConstant' shared_context nmi extracted_func
             =<< scTypeOf shared_context extracted_func
-          input_terms <- io $ traverse (scExtCns shared_context) input_parameters
+          input_terms <- io $ traverse (scVariable shared_context) input_parameters
           applied_extracted_func <- io $ scApplyAll shared_context extracted_func_const input_terms
           applied_extracted_func_selectors <-
             io $ forM [1 .. (length output_parameters)] $ \i ->
@@ -512,17 +512,17 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
           ps <- io (MS.mkProvedSpec MS.SpecProved extracted_method_spec stats vcs lemmaSet diff)
           returnLLVMProof (SomeLLVM ps)
 
-setupValueAsExtCns :: SetupValue (LLVM arch) -> Maybe (ExtCns Term)
-setupValueAsExtCns =
+setupValueAsVariable :: SetupValue (LLVM arch) -> Maybe (ExtCns Term)
+setupValueAsVariable =
   \case
-    SetupTerm term -> asExtCns $ ttTerm term
+    SetupTerm term -> asVariable $ ttTerm term
     _ -> Nothing
 
-llvmPointsToValueAsExtCns :: LLVMPointsToValue arch -> Maybe (ExtCns Term)
-llvmPointsToValueAsExtCns =
+llvmPointsToValueAsVariable :: LLVMPointsToValue arch -> Maybe (ExtCns Term)
+llvmPointsToValueAsVariable =
   \case
-    ConcreteSizeValue val -> setupValueAsExtCns val
-    SymbolicSizeValue arr _sz -> asExtCns $ ttTerm arr
+    ConcreteSizeValue val -> setupValueAsVariable val
+    SymbolicSizeValue arr _sz -> asVariable $ ttTerm arr
 
 -- | Check that all the overrides/lemmas were actually from this module
 checkModuleCompatibility ::
@@ -1599,7 +1599,7 @@ verifyPoststate cc mspec env0 globals ret mdMap invSubst =
            [ (ecVarIndex ec, ec)
            | tt <- mspec ^. MS.csPreState . MS.csFreshVars
            , let ec = tecExt tt ]
-     terms0 <- io $ traverse (scExtCns sc) ecs0
+     terms0 <- io $ traverse (scVariable sc) ecs0
 
      let initialFree =
            Set.fromList
@@ -1888,7 +1888,7 @@ setupArg sc sym ecRef tp = do
          let len = Seq.length ecs
          ec <- scFreshEC sc ("arg_" <> Text.pack (show len)) sc_tp
          writeIORef ecRef (ecs Seq.|> TypedExtCns cty ec)
-         scFlatTermF sc (ExtCns ec)
+         scVariable sc ec
 
 setupArgs ::
   SharedContext ->