Heapster: Add support for the trivially false permission

heapster-saw/examples/rust_data.rs

@@ -1,6 +1,10 @@
 use std::collections::{HashMap, HashSet};
 use std::fmt;
 
+/* A function that immediately panics */
+pub fn get_out () -> ! {
+    panic!("Uh oh!")
+}
 
 /* The logical and operation as a function on bool */
 pub fn bool_and (x:bool, y:bool) -> bool {

heapster-saw/examples/rust_data.saw

@@ -33,6 +33,10 @@ heapster_define_rust_type env "pub enum Sum<X,Y> { Left (X), Right (Y) }";
 // The Option type
 heapster_define_rust_type env "pub enum Option<X> { None, Some (X) }";
 
+// Location type from std::panic
+heapster_define_llvmshape env "panic::Location" 64 ""
+  "exsh len:bv 64.ptrsh(arraysh(<len,*1,fieldsh(8,int8<>))); fieldsh(eq(llvmword(len))); u32<>; u32<>";
+
 // The str type
 // For now we have to define the shape explicitly without the int8 name because
 // we don't yet have implications on array cells
@@ -395,10 +399,15 @@ Formatter__write_fmt_sym <- heapster_find_symbol env "9Formatter9write_fmt";
 heapster_assume_fun_rename_prim env Formatter__write_fmt_sym "Formatter__write_fmt"
   "<'a> fn (&'a mut fmt::Formatter, fmt::Arguments) -> fmt::Result";
 
+// std::panicking::begin_panic
+begin_panic_sym <- heapster_find_symbol env "3std9panicking11begin_panic17";
+heapster_assume_fun_rename_prim env begin_panic_sym "begin_panic" "<'a, 'b> fn(&'a str, &'b panic::Location) -> !";
 
 /***
  *** Type-Checked Functions
  ***/
+get_out_sym <- heapster_find_symbol env "7get_out";
+heapster_typecheck_fun_rename env get_out_sym "get_out" "<> fn() -> !";
 
 // bool_and
 bool_and_sym <- heapster_find_symbol env "8bool_and";

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

@@ -132,6 +132,7 @@ instance ContainsIRTRecName (ValuePerm a) where
     containsIRTRecName n args
   containsIRTRecName _ (ValPerm_Var _ _) = False
   containsIRTRecName n (ValPerm_Conj ps) = containsIRTRecName n ps
+  containsIRTRecName _ ValPerm_False = False
 
 instance ContainsIRTRecName (RAssign ValuePerm tps) where
   containsIRTRecName _ MNil = False
@@ -318,6 +319,7 @@ instance IRTTyVars (ValuePerm a) where
     [nuMP| ValPerm_Var x _ |] ->
       irtTTranslateVar mb_p x
     [nuMP| ValPerm_Conj ps |] -> irtTyVars ps
+    [nuMP| ValPerm_False |] -> return ([], IRTVarsNil)
 
 -- | Get all IRT type variables in a binding, including any type variables
 -- from the bound variable
@@ -468,6 +470,7 @@ instance IRTTyVars (PermExpr (LLVMShapeType w)) where
          (tps2, ixs2) <- irtTyVars sh2
          return (tps1 ++ tps2, IRTVarsAppend ixs1 ixs2)
     [nuMP| PExpr_ExShape sh |] -> irtTyVars sh -- see the instance for Binding!
+    [nuMP| PExpr_FalseShape |] -> return ([], IRTVarsNil)
 
 -- | Get all IRT type variables in a field shape
 instance IRTTyVars (LLVMFieldShape w) where

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

@@ -1131,6 +1131,13 @@ data SimplImpl ps_in ps_out where
     (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) -> LLVMBlockPerm w ->
     SimplImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w)
 
+  -- | Eliminate a block of shape @falsesh@ to @false@
+  --
+  -- > x:memblock(..., falsesh) -o x:false
+  SImpl_ElimLLVMBlockFalse ::
+    (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) -> LLVMBlockPerm w ->
+    SimplImpl (RNil :> LLVMPointerType w) (RNil :> LLVMPointerType w)
+
   -- | Fold a named permission (other than an opaque permission):
   --
   -- > x:(unfold P args) -o x:P<args>
@@ -1278,6 +1285,12 @@ data PermImpl1 ps_in ps_outs where
                       Binding tp (ValuePerm a) ->
                       PermImpl1 (ps :> a) (RNil :> '(RNil :> tp, ps :> a))
 
+  -- | Eliminate a @false@ permission on the top of the stack, which is a
+  -- contradiction and so has no output disjuncts
+  --
+  -- > ps * x:false -o .
+  Impl1_ElimFalse :: ExprVar a -> PermImpl1 (ps :> a) RNil
+
   -- | Apply a 'SimplImpl'
   Impl1_Simpl :: SimplImpl ps_in ps_out -> Proxy ps ->
                  PermImpl1 (ps :++: ps_in) (RNil :> '(RNil, ps :++: ps_out))
@@ -1622,6 +1635,7 @@ permImplSucceeds (PermImpl_Step (Impl1_ElimOr _ _ _)
 permImplSucceeds (PermImpl_Step (Impl1_ElimExists _ _)
                   (MbPermImpls_Cons _ _ mb_impl)) =
   mbLift $ fmap permImplSucceeds mb_impl
+permImplSucceeds (PermImpl_Step (Impl1_ElimFalse _) _) = 2
 permImplSucceeds (PermImpl_Step (Impl1_Simpl _ _)
                   (MbPermImpls_Cons _ _ mb_impl)) =
   mbLift $ fmap permImplSucceeds mb_impl
@@ -1949,6 +1963,8 @@ simplImplIn (SImpl_IntroLLVMBlockEx x bp) =
       error "simplImplIn: SImpl_IntroLLVMBlockEx: non-existential shape"
 simplImplIn (SImpl_ElimLLVMBlockEx x bp) =
   distPerms1 x (ValPerm_LLVMBlock bp)
+simplImplIn (SImpl_ElimLLVMBlockFalse x bp) =
+  distPerms1 x (ValPerm_LLVMBlock bp)
 simplImplIn (SImpl_FoldNamed x np args off) =
   distPerms1 x (unfoldPerm np args off)
 simplImplIn (SImpl_UnfoldNamed x np args off) =
@@ -2295,6 +2311,11 @@ simplImplOut (SImpl_ElimLLVMBlockEx x bp) =
                      ValPerm_LLVMBlock (bp { llvmBlockShape = sh }))
     _ ->
       error "simplImplOut: SImpl_ElimLLVMBlockEx: non-existential shape"
+simplImplOut (SImpl_ElimLLVMBlockFalse x bp) =
+  case llvmBlockShape bp of
+    PExpr_FalseShape ->
+      distPerms1 x ValPerm_False
+    _ -> error "simplImplOut: SImpl_ElimLLVMBlockFalse: non-false shape"
 simplImplOut (SImpl_FoldNamed x np args off) =
   distPerms1 x (ValPerm_Named (namedPermName np) args off)
 simplImplOut (SImpl_UnfoldNamed x np args off) =
@@ -2396,6 +2417,11 @@ applyImpl1 _ (Impl1_ElimExists x p_body) ps =
     mbPermSets1 (fmap (\p -> set (topDistPerm x) p ps) p_body)
   else
     error "applyImpl1: Impl1_ElimExists: unexpected permission"
+applyImpl1 _ (Impl1_ElimFalse x) ps =
+  if ps ^. topDistPerm x == ValPerm_False then
+    MbPermSets_Nil
+  else
+    error "applyImpl1: Impl1_ElimFalse: unexpected permission"
 applyImpl1 pp_info (Impl1_Simpl simpl prx) ps =
   mbPermSets1 $ emptyMb $ applySimplImpl pp_info prx simpl ps
 applyImpl1 _ (Impl1_LetBind tp e) ps =
@@ -2776,6 +2802,8 @@ instance SubstVar PermVarSubst m =>
       SImpl_IntroLLVMBlockEx <$> genSubst s x <*> genSubst s bp
     [nuMP| SImpl_ElimLLVMBlockEx x bp |] ->
       SImpl_ElimLLVMBlockEx <$> genSubst s x <*> genSubst s bp
+    [nuMP| SImpl_ElimLLVMBlockFalse x bp |] ->
+      SImpl_ElimLLVMBlockFalse <$> genSubst s x <*> genSubst s bp
     [nuMP| SImpl_FoldNamed x np args off |] ->
       SImpl_FoldNamed <$> genSubst s x <*> genSubst s np <*> genSubst s args
                       <*> genSubst s off
@@ -2822,6 +2850,8 @@ instance SubstVar PermVarSubst m =>
       Impl1_ElimOr <$> genSubst s x <*> genSubst s p1 <*> genSubst s p2
     [nuMP| Impl1_ElimExists x p_body |] ->
       Impl1_ElimExists <$> genSubst s x <*> genSubst s p_body
+    [nuMP| Impl1_ElimFalse x |] ->
+      Impl1_ElimFalse <$> genSubst s x
     [nuMP| Impl1_Simpl simpl prx |] ->
       Impl1_Simpl <$> genSubst s simpl <*> return (mbLift prx)
     [nuMP| Impl1_LetBind tp e |] ->
@@ -3405,6 +3435,12 @@ implElimExistsM x p =
   implApplyImpl1 (Impl1_ElimExists x p)
   (MNil :>: Impl1Cont (const $ pure ()))
 
+-- | Eliminate a false permission in the current permission set
+implElimFalseM :: NuMatchingAny1 r => ExprVar a ->
+                  ImplM vars s r ps_any (ps :> a) ()
+implElimFalseM x =
+  implApplyImpl1 (Impl1_ElimFalse x) MNil
+
 -- | Apply a simple implication rule to the top permissions on the stack
 implSimplM :: HasCallStack => NuMatchingAny1 r => Proxy ps ->
               SimplImpl ps_in ps_out ->
@@ -4704,6 +4740,10 @@ implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
                                         PExpr_ExShape _mb_sh }) =
   implSimplM Proxy (SImpl_ElimLLVMBlockEx x bp)
 
+implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
+                                        PExpr_FalseShape }) =
+  implSimplM Proxy (SImpl_ElimLLVMBlockFalse x bp)
+
 -- If none of the above cases matched, we cannot eliminate, so fail
 implElimLLVMBlock _ bp =
   implTraceM (\i -> pretty "Could not eliminate permission" <+>
@@ -4967,6 +5007,7 @@ recombinePermExpl x x_p p =
 recombinePerm' :: NuMatchingAny1 r => ExprVar a -> ValuePerm a -> ValuePerm a ->
                   ImplM vars s r as (as :> a) ()
 recombinePerm' x _ p@ValPerm_True = implDropM x p
+recombinePerm' x _ ValPerm_False = implElimFalseM x
 recombinePerm' x _ p@(ValPerm_Eq (PExpr_Var y)) | y == x = implDropM x p
 recombinePerm' x ValPerm_True (ValPerm_Eq e) =
   simplEqPerm x e >>>= \e' -> implPopM x (ValPerm_Eq e')
@@ -5090,6 +5131,12 @@ recombinePermConj x x_ps (Perm_LLVMBlock bp)
     getTopDistPerm x >>>= \p ->
     recombinePerm x p
 
+-- If p is a memblock permission on the false shape, eliminate the block to
+-- a false permission (and eliminate the false permission itself)
+recombinePermConj x _ (Perm_LLVMBlock bp)
+  | PExpr_FalseShape <- llvmBlockShape bp
+  = implElimLLVMBlock x bp >>> implElimFalseM x
+
 -- Default case: insert p at the end of the x_ps
 recombinePermConj x x_ps p =
   implPushM x (ValPerm_Conj x_ps) >>>

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

@@ -16,6 +16,7 @@ import Control.Monad.Reader
 import GHC.TypeLits
 import qualified Text.PrettyPrint.HughesPJ as PPHPJ
 
+import qualified Data.BitVector.Sized as BV
 import qualified Text.LLVM.AST as L
 import qualified Text.LLVM.PP as L
 
@@ -118,14 +119,25 @@ translateLLVMValue w _ (L.ValPackedStruct elems) =
   mapM (translateLLVMTypedValue w) elems >>= \(unzip -> (shs,ts)) ->
   return (foldr PExpr_SeqShape PExpr_EmptyShape shs, tupleOpenTerm ts)
 translateLLVMValue _ _ (L.ValString []) = mzero
+translateLLVMValue _ _ (L.ValString bytes) =
+  let sh =
+        foldr1 PExpr_SeqShape $
+        map (PExpr_FieldShape . LLVMFieldShape . ValPerm_Eq .
+             PExpr_LLVMWord . bvBV . BV.word8) bytes in
+  return (sh, unitOpenTerm)
+-- NOTE: we don't translate strings to one big bitvector value because that
+-- seems to mess up the endianness
+{-
 translateLLVMValue _ _ (L.ValString bytes) =
   do endianness <- llvmTransInfoEndianness <$> ask
      case bvFromBytes endianness bytes of
        Some (BVExpr e) ->
          return (PExpr_FieldShape (LLVMFieldShape $
                                    ValPerm_Eq $ PExpr_LLVMWord e),
                  unitOpenTerm)
-
+-}
+-- NOTE: we don't convert string values to arrays because we sometimes need to
+-- statically know the values of the bytes in a string value as eq perms
 {-
 translateLLVMValue w tp (L.ValString bytes) =
   translateLLVMValue w tp (L.ValArray