Merge pull request #2757 from GaloisInc/bh/issue2749

Avoid applying Nat recursor to bvToNat.

Author: brianhuffman

intTests/test2749/test.saw

@@ -0,0 +1,16 @@
+// test.saw
+enable_experimental;
+
+let
+{{
+inc : [1024][8] -> [64] -> [1024][8]
+inc arr idx = update arr idx (arr @ idx + 10)
+}};
+
+prove_print
+  do {
+    print_goal;
+    goal_normalize [];
+    z3;
+  }
+  {{ \arr_val -> inc arr_val 0 == update arr_val 0 (arr_val @ 0 + 10) }};

intTests/test2749/test.sh

@@ -0,0 +1,2 @@
+#!/bin/sh
+$SAW test.saw

saw-central/src/SAWCentral/Builtins.hs

@@ -25,6 +25,7 @@ import qualified Data.ByteString.Lazy as BS
 import qualified Data.IntMap as IntMap
 import Data.List (isPrefixOf, isInfixOf, sort, intersperse)
 import qualified Data.Map as Map
+import Data.Maybe (catMaybes)
 import Data.Parameterized.Classes (KnownRepr(..))
 import Data.Set (Set)
 import qualified Data.Set as Set
@@ -63,9 +64,10 @@ import SAWCore.ExternalFormat
 import SAWCore.FiniteValue
   ( FiniteType(..), readFiniteValue
   )
-import SAWCore.Name (ModuleName, VarName(..), mkModuleName)
+import SAWCore.Name (ModuleName, VarName(..), mkModuleName, moduleIdentToURI)
 import SAWCore.SATQuery
 import SAWCore.SCTypeCheck
+import SAWCore.Simulator.Concrete (constMap)
 import SAWCore.Recognizer
 import SAWCore.Prelude (scEq)
 import SAWCore.SharedTerm
@@ -571,7 +573,10 @@ goal_normalize opaque =
   execTactic $ tacticChange $ \goal ->
     do sc <- getSharedContext
        idxs <- mconcat <$> mapM (resolveName sc) opaque
-       let opaqueSet = Set.fromList idxs
+       -- Also exclude defined SAWCore constants that are implemented as primitives
+       let primURIs = map moduleIdentToURI (Map.keys constMap)
+       primIdxs <- io $ traverse (scResolveNameByURI sc) primURIs
+       let opaqueSet = Set.fromList (catMaybes primIdxs ++ idxs)
        sqt' <- io $ traverseSequentWithFocus (normalizeProp sc opaqueSet) (goalSequent goal)
        return (sqt', NormalizePropEvidence opaqueSet)
 

saw-core/src/SAWCore/Simulator.hs

@@ -251,6 +251,9 @@ evalTermF cfg lam recEval tf env =
             VCtorMux _ps branches ->
               do alts <- traverse (evalCtorMuxBranch vrec) (IntMap.elems branches)
                  combineAlts alts
+            VBVToNat{} ->
+              panic "evalTerF / evalRecursor"
+              ["Unsupported symbolic recursor argument of type Nat"]
             _ ->
               panic "evalTermF / evalRecursor"
               ["Expected constructor for datatype: " <> toAbsoluteName (nameInfo d)]

saw-core/src/SAWCore/Simulator/Concrete.hs

@@ -17,6 +17,7 @@ module SAWCore.Simulator.Concrete
        , toBool
        , toWord
        , runIdentity
+       , constMap
        ) where
 
 import Control.Monad.Identity