More Heapster rust typechecking bugs

heapster-saw/examples/rust_data.saw

@@ -521,23 +521,23 @@ heapster_typecheck_fun_rename env bintree_is_leaf_sym "bintree_is_leaf"
   "<'a> fn (t: &'a BinTree<u64>) -> bool";
 
 enum20_list_proj_sym <- heapster_find_symbol env "16enum20_list_proj";
-//heapster_typecheck_fun_rename env enum20_list_proj_sym "enum20_list_proj"
+heapster_typecheck_fun_rename env enum20_list_proj_sym "enum20_list_proj"
   "<'a> fn (x:&'a Enum20<List<u64>>) -> &'a List<u64>";
 
 list10_head_sym <- heapster_find_symbol env "11list10_head";
-//heapster_typecheck_fun_rename env list10_head_sym "list10_head"
+heapster_typecheck_fun_rename env list10_head_sym "list10_head"
   "<'a> fn (x:&'a List10<List<u64>>) -> &'a List<u64>";
 
 list20_u64_clone_sym <- heapster_find_symbol env
   "List20$LT$u64$GT$$u20$as$u20$core..clone..Clone$GT$5clone";
 heapster_typecheck_fun_rename env list20_u64_clone_sym "list20_u64_clone"
   "<'a> fn (&'a List20<u64>) -> List20<u64>";
 
-/*
+heapster_set_translation_checks env false;
 list20_head_sym <- heapster_find_symbol env "11list20_head";
 heapster_typecheck_fun_rename env list20_head_sym "list20_head"
   "<'a> fn (x:&'a List20<List<u64>>) -> &'a List<u64>";
-*/
+
 
 /***
  *** Export to Coq

heapster-saw/src/Verifier/SAW/Heapster/Implication.hs

@@ -6898,12 +6898,17 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps
   , Just off <- partialSubst psubst (mbLLVMBlockOffset mb_bp)
   , Just len <- partialSubst psubst (mbLLVMBlockLen mb_bp)
   , Just i <- findIndex (llvmPermContainsOffsetBool off) ps
-  , (Perm_LLVMField (fp :: LLVMFieldPerm w sz)) <- ps!!i
-  , bvLeq (bvAdd off len) (bvAdd (llvmFieldOffset fp) (llvmFieldLen fp)) =
+  , Perm_LLVMField fp <- ps!!i
+  , len1 <- bvSub (llvmFieldEndOffset fp) off
+  , bvLeq len len1
+  , Just len1_int <- bvMatchConstInt len1
+  , Just (Some (sz1 :: NatRepr sz1)) <- someNat (8 * len1_int)
+  , Left LeqProof <- decideLeq (knownNat @1) sz1 =
 
     -- Recursively prove a membblock with shape fieldsh(eq(y)) for fresh evar y
+    withKnownNat sz1 $
     let mb_bp' =
-          mbCombine (MNil :>: (Proxy :: Proxy (LLVMPointerType sz))) $
+          mbCombine (MNil :>: (Proxy :: Proxy (LLVMPointerType sz1))) $
           mbMapCl $(mkClosed
                     [| \bp -> nu $ \y ->
                       bp { llvmBlockShape =
@@ -6969,9 +6974,8 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps
   , Just off <- partialSubst psubst (mbLLVMBlockOffset mb_bp)
   , Just len <- partialSubst psubst (mbLLVMBlockLen mb_bp)
   , Just i <- findIndex (llvmPermContainsOffsetBool off) ps
-  , Just off_lhs <- llvmAtomicPermOffset (ps!!i)
-  , Just len_lhs <- llvmAtomicPermLen (ps!!i)
-  , len1 <- bvSub len_lhs (bvSub off off_lhs)
+  , Just end_lhs <- llvmAtomicPermEndOffset (ps!!i)
+  , len1 <- bvSub end_lhs off
   , bvLt len1 len =
 
     -- Build existential memblock perms with fresh variables for shapes, where

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -1834,6 +1834,16 @@ llvmFieldSize _ = knownNat
 llvmFieldSizeBytes :: KnownNat sz => LLVMFieldPerm w sz -> Integer
 llvmFieldSizeBytes fp = intValue (llvmFieldSize fp) `ceil_div` 8
 
+-- | Get the size of an 'LLVMFieldPerm' as an expression
+llvmFieldLen :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>
+                LLVMFieldPerm w sz -> PermExpr (BVType w)
+llvmFieldLen fp = exprLLVMTypeBytesExpr $ llvmFieldContents fp
+
+-- | Get the ending offset of an 'LLVMFieldPerm'
+llvmFieldEndOffset :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>
+                      LLVMFieldPerm w sz -> PermExpr (BVType w)
+llvmFieldEndOffset fp = bvAdd (llvmFieldOffset fp) (llvmFieldLen fp)
+
 -- | Helper to get a 'NatRepr' for the size of an 'LLVMFieldPerm' in a binding
 mbLLVMFieldSize :: KnownNat sz => Mb ctx (LLVMFieldPerm w sz) -> NatRepr sz
 mbLLVMFieldSize _ = knownNat
@@ -3224,11 +3234,6 @@ isLLVMAtomicPermWithOffset off p
   | Just off' <- llvmAtomicPermOffset p = bvEq off off'
 isLLVMAtomicPermWithOffset _ _ = False
 
--- | Get the size of an 'LLVMFieldPerm' as an expression
-llvmFieldLen :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) =>
-                LLVMFieldPerm w sz -> PermExpr (BVType w)
-llvmFieldLen fp = exprLLVMTypeBytesExpr $ llvmFieldContents fp
-
 -- | Test if an 'AtomicPerm' is an array permission
 isLLVMArrayPerm :: AtomicPerm a -> Bool
 isLLVMArrayPerm (Perm_LLVMArray _) = True
@@ -3683,6 +3688,14 @@ llvmAtomicPermLen (Perm_LLVMArray ap) = Just $ llvmArrayLengthBytes ap
 llvmAtomicPermLen (Perm_LLVMBlock bp) = Just $ llvmBlockLen bp
 llvmAtomicPermLen _ = Nothing
 
+-- | Get the ending offset of an atomic permission, if it has one. This
+-- includes array permissions which may have some cells borrowed.
+llvmAtomicPermEndOffset :: (1 <= w, KnownNat w) =>
+                           AtomicPerm (LLVMPointerType w) ->
+                           Maybe (PermExpr (BVType w))
+llvmAtomicPermEndOffset p =
+  bvAdd <$> llvmAtomicPermOffset p <*> llvmAtomicPermLen p
+
 -- | Get the range of offsets of an atomic permission, if it has one. Note that
 -- arrays with borrows do not have a well-defined range.
 llvmAtomicPermRange :: AtomicPerm (LLVMPointerType w) -> Maybe (BVRange w)

src/SAWScript/HeapsterBuiltins.hs

@@ -41,6 +41,9 @@ module SAWScript.HeapsterBuiltins
        , heapster_join_point_hint
        , heapster_find_symbol
        , heapster_find_symbols
+       , heapster_find_symbol_with_type
+       , heapster_find_symbols_with_type
+       , heapster_find_symbol_commands
        , heapster_find_trait_method_symbol
        , heapster_assume_fun
        , heapster_assume_fun_rename
@@ -99,6 +102,9 @@ import Lang.Crucible.LLVM.TypeContext
 import Lang.Crucible.LLVM.DataLayout
 
 import qualified Text.LLVM.AST as L
+import qualified Text.LLVM.Parser as L
+import qualified Text.LLVM.PP as L
+import qualified Text.PrettyPrint.HughesPJ as L (render)
 
 import SAWScript.TopLevel
 import SAWScript.Value
@@ -874,6 +880,93 @@ heapster_find_symbol bic opts henv str =
     _ -> fail ("Found multiple symbols matching string " ++ str ++ ": " ++
                concat (intersperse ", " $ map show syms))
 
+-- | Extract the 'String' name of an LLVM symbol
+symString :: L.Symbol -> String
+symString (L.Symbol str) = str
+
+-- | Extract the function type of an LLVM definition
+defFunType :: L.Define -> L.Type
+defFunType defn =
+  L.FunTy (L.defRetType defn) (map L.typedType
+                               (L.defArgs defn)) (L.defVarArgs defn)
+
+-- | Extract the function type of an LLVM declaration
+decFunType :: L.Declare -> L.Type
+decFunType decl =
+  L.FunTy (L.decRetType decl) (L.decArgs decl) (L.decVarArgs decl)
+
+-- | Search for all symbols with the supplied string as a substring that have
+-- the supplied LLVM type
+heapster_find_symbols_with_type :: BuiltinContext -> Options -> HeapsterEnv ->
+                                   String -> String -> TopLevel [String]
+heapster_find_symbols_with_type _bic _opts henv str tp_str =
+  case L.parseType tp_str of
+    Left err ->
+      fail ("Error parsing LLVM type: " ++ tp_str ++ "\n" ++ show err)
+    Right tp@(L.FunTy _ _ _) ->
+      return $
+      concatMap (\(Some lm) ->
+                  mapMaybe (\decl ->
+                             if isInfixOf str (symString $ L.decName decl) &&
+                                decFunType decl == tp
+                             then Just (symString $ L.decName decl) else Nothing)
+                  (L.modDeclares $ modAST lm)
+                  ++
+                  mapMaybe (\defn ->
+                             if isInfixOf str (symString $ L.defName defn) &&
+                                defFunType defn == tp
+                             then Just (symString $ L.defName defn) else Nothing)
+                  (L.modDefines $ modAST lm)) $
+      heapsterEnvLLVMModules henv
+    Right tp ->
+      fail ("Expected an LLVM function type, but found: " ++ show tp)
+
+-- | Search for a symbol by name and Crucible type in any LLVM module in a
+-- 'HeapsterEnv' that contains the supplied string as a substring
+heapster_find_symbol_with_type :: BuiltinContext -> Options -> HeapsterEnv ->
+                                  String -> String -> TopLevel String
+heapster_find_symbol_with_type bic opts henv str tp_str =
+  heapster_find_symbols_with_type bic opts henv str tp_str >>= \syms ->
+  case syms of
+    [sym] -> return sym
+    [] -> fail ("No symbol found matching string: " ++ str ++
+                " and type: " ++ tp_str)
+    _ -> fail ("Found multiple symbols matching string " ++ str ++
+               " and type: " ++ tp_str ++ ": " ++
+               concat (intersperse ", " $ map show syms))
+
+-- | Print a 'String' as a SAW-script string literal, escaping any double quotes
+-- or newlines
+print_as_saw_script_string :: String -> String
+print_as_saw_script_string str =
+  "\"" ++ concatMap (\c -> case c of
+                        '\"' -> "\\\""
+                        '\n' -> "\\\n\\"
+                        _ -> [c]) str ++ "\"";
+
+-- | Map a search string @str@ to a newline-separated sequence of SAW-script
+-- commands @"heapster_find_symbol_with_type str tp"@, one for each LLVM type
+-- @tp@ associated with a symbol whose name contains @str@
+heapster_find_symbol_commands :: BuiltinContext -> Options -> HeapsterEnv ->
+                                 String -> TopLevel String
+heapster_find_symbol_commands _bic _opts henv str =
+  return $
+  concatMap (\tp ->
+              "heapster_find_symbol_with_type env\n  \"" ++ str ++ "\"\n  " ++
+              print_as_saw_script_string (L.render $ L.ppType tp) ++ ";\n") $
+  concatMap (\(Some lm) ->
+              mapMaybe (\decl ->
+                         if isInfixOf str (symString $ L.decName decl)
+                         then Just (decFunType decl)
+                         else Nothing)
+              (L.modDeclares $ modAST lm)
+              ++
+              mapMaybe (\defn ->
+                         if isInfixOf str (symString $ L.defName defn)
+                         then Just (defFunType defn) else Nothing)
+              (L.modDefines $ modAST lm)) $
+  heapsterEnvLLVMModules henv
+
 -- | Search for a symbol name in any LLVM module in a 'HeapsterEnv' that
 -- corresponds to the supplied string, which should be of the form:
 -- "trait::method<type>". Fails if there is not exactly one such symbol.

src/SAWScript/Interpreter.hs

@@ -3227,6 +3227,32 @@ primitives = Map.fromList
     , " contain the supplied string as a substring"
     ]
 
+  , prim "heapster_find_symbol_with_type"
+    "HeapsterEnv -> String -> String -> TopLevel String"
+    (bicVal heapster_find_symbol_with_type)
+    Experimental
+    [ "Search for a symbol in any module contained in a HeapsterEnv that"
+    , " contains the supplied string as a substring and that has the specified"
+    , " LLVM type. Raise an error if there is not exactly one such symbol."
+    ]
+
+  , prim "heapster_find_symbols_with_type"
+    "HeapsterEnv -> String -> String -> TopLevel [String]"
+    (bicVal heapster_find_symbols_with_type)
+    Experimental
+    [ "Search for all symbols in any module contained in a HeapsterEnv that"
+    , " contain the supplied string as a substring and that have the specified"
+    , " LLVM type"
+    ]
+
+  , prim "heapster_find_symbol_commands"
+    "HeapsterEnv -> String -> TopLevel [String]"
+    (bicVal heapster_find_symbol_commands)
+    Experimental
+    [ "Map a search string str to a newline-separated sequence of SAW-script "
+    , " commands \"heapster_find_symbol_with_type str tp\", one for each LLVM "
+    , " type tp associated with a symbol whose name contains str" ]
+
   , prim "heapster_find_trait_method_symbol"
     "HeapsterEnv -> String -> TopLevel String"
     (bicVal heapster_find_trait_method_symbol)