Merge pull request #1679 from GaloisInc/rwd/goal-metadata

Goal metadata

CHANGES.md

@@ -47,6 +47,23 @@
   required to provide a term that describes how the live variables in
   the loop evolve over an iteration.
 
+* A new experimental facility for "tagging" proof obligations in
+  specifications and later using those tags to make decisions
+  in proof tactics. See the new `llvm_setup_with_tag`,
+  `goal_has_tags`, and `goal_has_some_tag` commands.
+
+* A new experimental option (toggled via
+  `enable_single_override_special_case` and
+  `disable_single_override_special_case`) which changes the handling
+  for cases where an overriden function has only one override that
+  could possibly apply. When the special case handling is enabled,
+  preconditions for the override are asserted separately, maintaining
+  their individual metadata instead of being combined into a single
+  precondition for the entire override. This may be advantageous if
+  proving the individual goals is easier than the conjunction of all
+  of them, or if different tactics are needed for different subgoals.
+  Currently, this option only applies to LLVM verifications.
+
 # Version 0.9
 
 ## New Features

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

@@ -342,7 +342,13 @@ gatherAssumes msb =
     let loc = msb ^. msbSpec . MS.csLoc
     assumeConds <- liftIO $ forM assumes' $ \pred -> do
         tt <- eval pred >>= SAW.mkTypedTerm sc
-        return $ MS.SetupCond_Pred loc tt
+        let md = MS.ConditionMetadata
+                 { MS.conditionLoc = loc
+                 , MS.conditionTags = mempty
+                 , MS.conditionType = "specification assertion"
+                 , MS.conditionContext = ""
+                 }
+        return $ MS.SetupCond_Pred md tt
     newVars <- liftIO $ gatherVars sym [Some (MethodSpecValue BoolRepr pred) | pred <- assumes']
 
     return $ msb
@@ -396,7 +402,13 @@ gatherAsserts msb =
     let loc = msb ^. msbSpec . MS.csLoc
     assertConds <- liftIO $ forM asserts'' $ \pred -> do
         tt <- eval pred >>= SAW.mkTypedTerm sc
-        return $ MS.SetupCond_Pred loc tt
+        let md = MS.ConditionMetadata
+                 { MS.conditionLoc = loc
+                 , MS.conditionTags = mempty
+                 , MS.conditionType = "specification condition"
+                 , MS.conditionContext = ""
+                 }
+        return $ MS.SetupCond_Pred md tt
 
     return $ msb
         & msbSpec . MS.csPostState . MS.csConditions %~ (++ assertConds)

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

@@ -191,7 +191,13 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->
                     ": no arg at index " ++ show i
                 Just x -> return x
             let shp = tyToShapeEq col ty tpr
-            matchArg sym sc eval (ms ^. MS.csPreState . MS.csAllocs) shp rv sv
+            let md = MS.ConditionMetadata
+                     { MS.conditionLoc = loc
+                     , MS.conditionTags = mempty
+                     , MS.conditionType = "formal argument matching"
+                     , MS.conditionContext = ""
+                     }
+            matchArg sym sc eval (ms ^. MS.csPreState . MS.csAllocs) md shp rv sv
 
         -- Match PointsTo SetupValues against accessible memory.
         --
@@ -216,8 +222,13 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->
                 ref' <- lift $ mirRef_offsetSim (ptr ^. mpType) (ptr ^. mpRef) iSym
                 rv <- lift $ readMirRefSim (ptr ^. mpType) ref'
                 let shp = tyToShapeEq col ty (ptr ^. mpType)
-                matchArg sym sc eval (ms ^. MS.csPreState . MS.csAllocs) shp rv sv
-
+                let md = MS.ConditionMetadata
+                         { MS.conditionLoc = loc
+                         , MS.conditionTags = mempty
+                         , MS.conditionType = "points-to"
+                         , MS.conditionContext = ""
+                         }
+                matchArg sym sc eval (ms ^. MS.csPreState . MS.csAllocs) md shp rv sv
 
         -- Validity checks
 
@@ -248,26 +259,27 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->
 
         -- Convert preconditions to `osAsserts`
         forM_ (ms ^. MS.csPreState . MS.csConditions) $ \cond -> do
-            term <- condTerm sc cond
+            (md, term) <- condTerm sc cond
             w4VarMap <- liftIO $ readIORef w4VarMapRef
             pred <- liftIO $ termToPred sym sc w4VarMap term
-            MS.addAssert pred $
+            MS.addAssert pred md $
                 SimError loc (AssertFailureSimError (show $ W4.printSymExpr pred) "")
 
         -- Convert postconditions to `osAssumes`
         forM_ (ms ^. MS.csPostState . MS.csConditions) $ \cond -> do
-            term <- condTerm sc cond
+            (md, term) <- condTerm sc cond
             w4VarMap <- liftIO $ readIORef w4VarMapRef
             pred <- liftIO $ termToPred sym sc w4VarMap term
-            MS.addAssume pred
+            MS.addAssume pred md
 
     ((), os) <- case result of
         Left err -> error $ show err
         Right x -> return x
 
-    forM_ (os ^. MS.osAsserts) $ \lp ->
+    forM_ (os ^. MS.osAsserts) $ \(_md, lp) ->
+      -- TODO, track metadata
       liftIO $ addAssertion bak lp
-    forM_ (os ^. MS.osAssumes) $ \p ->
+    forM_ (os ^. MS.osAssumes) $ \(_md, p) ->
       liftIO $ addAssumption bak (GenericAssumption loc "methodspec postcondition" p)
 
     let preAllocMap = os ^. MS.setupValueSub
@@ -337,9 +349,10 @@ matchArg ::
     SAW.SharedContext ->
     (forall tp'. W4.Expr t tp' -> IO SAW.Term) ->
     Map MS.AllocIndex (Some MirAllocSpec) ->
+    MS.ConditionMetadata ->
     TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR ->
     MirOverrideMatcher sym ()
-matchArg sym sc eval allocSpecs shp rv sv = go shp rv sv
+matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
   where
     go :: forall tp. TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR ->
         MirOverrideMatcher sym ()
@@ -372,7 +385,7 @@ matchArg sym sc eval allocSpecs shp rv sv = go shp rv sv
                         show (W4.exprType expr) ++ " doesn't match SetupValue type " ++
                         show (W4.exprType val)
                 eq <- liftIO $ W4.isEq sym expr val
-                MS.addAssert eq $ SimError loc $
+                MS.addAssert eq md $ SimError loc $
                     AssertFailureSimError
                         ("mismatch on " ++ show (W4.exprType expr) ++ ": expected " ++
                             show (W4.printSymExpr val))
@@ -467,7 +480,7 @@ matchArg sym sc eval allocSpecs shp rv sv = go shp rv sv
                 eq <- lift $ ovrWithBackend $ \bak ->
                         liftIO $ mirRef_eqIO bak ref' (ptr ^. mpRef)
                 let loc = mkProgramLoc "matchArg" InternalPos
-                MS.addAssert eq $
+                MS.addAssert eq md $
                     SimError loc (AssertFailureSimError ("mismatch on " ++ show alloc) "")
               | otherwise -> error $ "mismatched types for " ++ show alloc ++ ": " ++
                     show tpr ++ " does not match " ++ show (ptr ^. mpType)
@@ -543,13 +556,13 @@ condTerm ::
     (IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     SAW.SharedContext ->
     MS.SetupCondition MIR ->
-    MirOverrideMatcher sym SAW.Term
+    MirOverrideMatcher sym (MS.ConditionMetadata, SAW.Term)
 condTerm _sc (MS.SetupCond_Equal _loc _sv1 _sv2) = do
     error $ "learnCond: SetupCond_Equal NYI" -- TODO
-condTerm sc (MS.SetupCond_Pred _loc tt) = do
+condTerm sc (MS.SetupCond_Pred md tt) = do
     sub <- use MS.termSub
     t' <- liftIO $ SAW.scInstantiateExt sc sub $ SAW.ttTerm tt
-    return t'
+    return (md, t')
 condTerm _ (MS.SetupCond_Ghost _ _ _ _) = do
     error $ "learnCond: SetupCond_Ghost is not supported"
 

intTests/test_goal_tags_01/Makefile

@@ -0,0 +1,17 @@
+.PHONY: all clean
+
+CC ?= clang
+CFLAGS ?= -O0 -emit-llvm
+SAW ?= saw
+
+all: test.bc
+	$(SAW) test.saw
+
+clean:
+	rm -f *.bc *.ll *.log
+
+%.bc: %.c
+	$(CC) $(CFLAGS) -g -c -o $@ $^
+
+%.ll: %.c
+	$(CC) $(CFLAGS) -g -c -S -o $@ $^

intTests/test_goal_tags_01/README

@@ -0,0 +1,6 @@
+This is a simple test of the "goal tagging" instructions.
+
+The test is setup to produce two tagged goals, and the tags are used
+by the proof tactic uses to select a proving method.  Any additional
+goals are ignored, and should lead to a proof failure. This test
+ensures the goals are being correctly tagged and filtered.

intTests/test_goal_tags_01/test.c

@@ -0,0 +1,5 @@
+
+unsigned int f(unsigned int i)
+{
+  return (i+1);
+}

intTests/test_goal_tags_01/test.ll

@@ -0,0 +1,43 @@
+; ModuleID = 'test.c'
+source_filename = "test.c"
+target datalayout = "e-m:o-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-apple-macosx11.0.0"
+
+; Function Attrs: noinline nounwind optnone ssp uwtable
+define i32 @f(i32 %0) #0 !dbg !9 {
+  %2 = alloca i32, align 4
+  store i32 %0, i32* %2, align 4
+  call void @llvm.dbg.declare(metadata i32* %2, metadata !13, metadata !DIExpression()), !dbg !14
+  %3 = load i32, i32* %2, align 4, !dbg !15
+  %4 = add i32 %3, 1, !dbg !16
+  ret i32 %4, !dbg !17
+}
+
+; Function Attrs: nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+attributes #0 = { noinline nounwind optnone ssp uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "darwin-stkchk-strong-link" "disable-tail-calls"="false" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "probe-stack"="___chkstk_darwin" "stack-protector-buffer-size"="8" "target-cpu"="penryn" "target-features"="+cx16,+cx8,+fxsr,+mmx,+sahf,+sse,+sse2,+sse3,+sse4.1,+ssse3,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+attributes #1 = { nounwind readnone speculatable willreturn }
+
+!llvm.module.flags = !{!0, !1, !2, !3, !4}
+!llvm.dbg.cu = !{!5}
+!llvm.ident = !{!8}
+
+!0 = !{i32 2, !"SDK Version", [2 x i32] [i32 12, i32 1]}
+!1 = !{i32 7, !"Dwarf Version", i32 4}
+!2 = !{i32 2, !"Debug Info Version", i32 3}
+!3 = !{i32 1, !"wchar_size", i32 4}
+!4 = !{i32 7, !"PIC Level", i32 2}
+!5 = distinct !DICompileUnit(language: DW_LANG_C99, file: !6, producer: "Apple clang version 12.0.5 (clang-1205.0.22.11)", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, enums: !7, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX12.1.sdk", sdk: "MacOSX12.1.sdk")
+!6 = !DIFile(filename: "test.c", directory: "/Users/rdockins/code/saw-script/intTests/test_goal_tags_01")
+!7 = !{}
+!8 = !{!"Apple clang version 12.0.5 (clang-1205.0.22.11)"}
+!9 = distinct !DISubprogram(name: "f", scope: !6, file: !6, line: 2, type: !10, scopeLine: 3, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !5, retainedNodes: !7)
+!10 = !DISubroutineType(types: !11)
+!11 = !{!12, !12}
+!12 = !DIBasicType(name: "unsigned int", size: 32, encoding: DW_ATE_unsigned)
+!13 = !DILocalVariable(name: "i", arg: 1, scope: !9, file: !6, line: 2, type: !12)
+!14 = !DILocation(line: 2, column: 29, scope: !9)
+!15 = !DILocation(line: 4, column: 11, scope: !9)
+!16 = !DILocation(line: 4, column: 12, scope: !9)
+!17 = !DILocation(line: 4, column: 3, scope: !9)

intTests/test_goal_tags_01/test.saw

@@ -0,0 +1,37 @@
+enable_experimental;
+
+let f_spec : CrucibleSetup () = llvm_setup_with_tag "f spec" do {
+  i <- llvm_fresh_var "i" (llvm_int 32);
+  llvm_precond {{i < 512}};
+  llvm_execute_func [llvm_term i];
+
+  j <- llvm_fresh_var "j" (llvm_int 32);
+  llvm_return (llvm_term j);
+  llvm_setup_with_tag "post bound"
+    (llvm_postcond {{ j <= 512 }});
+  llvm_setup_with_tag "post eq"
+    (llvm_postcond {{ j == i+1 }});
+};
+
+let tac : ProofScript () = do {
+  isBound <- goal_has_tags ["post bound", "f spec"];
+  isEq    <- goal_has_tags ["post eq", "f spec"];
+
+  if isBound then do {
+    print_goal_summary;
+    yices;
+  } else if isEq then do {
+    print_goal_summary;
+    z3;
+  } else do {
+    // empty tactic should fail here if there are any goals
+    // not handled by the above
+    return ();
+  };
+};
+
+let main : TopLevel () = do {
+  m <- llvm_load_module "test.bc";
+  llvm_verify m "f" [] false f_spec tac;
+  print "done";
+};

intTests/test_goal_tags_01/test.sh

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

saw-remote-api/src/SAWServer.hs

@@ -241,6 +241,7 @@ initialState readFileFn =
                 , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout
                 , rwPathSatSolver = CC.PathSat_Z3
                 , rwSkipSafetyProofs = False
+                , rwSingleOverrideSpecialCase = False
                 }
      return (SAWState emptyEnv bic [] ro rw M.empty)
 

src/SAWScript/Builtins.hs

@@ -429,10 +429,15 @@ print_term_depth d t =
      printOutLnTop Info output
 
 goalSummary :: ProofGoal -> String
-goalSummary goal = unlines $
-  [ ("Goal " ++ goalName goal ++ " (goal number " ++ (show $ goalNum goal) ++ "): " ++ goalType goal) ++ " at " ++ goalLoc goal ] ++
-  if null (goalDesc goal) then [] else [ goalDesc goal ]
-
+goalSummary goal = unlines $ concat
+  [ [ "Goal " ++ goalName goal ++ " (goal number " ++ (show $ goalNum goal) ++ "): " ++ goalType goal
+    , "at " ++ goalLoc goal
+    ]
+  , if Set.null (goalTags goal) then [] else
+      [ unwords ("Tags:" : map show (Set.toList (goalTags goal)))
+      ]
+  , if null (goalDesc goal) then [] else [ goalDesc goal ]
+  ]
 
 write_goal :: String -> ProofScript ()
 write_goal fp =
@@ -693,6 +698,20 @@ goal_when str script =
        g : _ | str `isInfixOf` goalName g -> script
        _ -> return ()
 
+goal_has_tags :: [String] -> ProofScript Bool
+goal_has_tags tags =
+  do s <- get
+     case psGoals s of
+       g : _ | Set.isSubsetOf (Set.fromList tags) (goalTags g) -> return True
+       _ -> return False  
+
+goal_has_some_tag :: [String] -> ProofScript Bool
+goal_has_some_tag tags =
+  do s <- get
+     case psGoals s of
+       g : _ | not $ Set.disjoint (Set.fromList tags) (goalTags g) -> return True
+       _ -> return False  
+
 goal_num_ite :: Int -> ProofScript SV.Value -> ProofScript SV.Value -> ProofScript SV.Value
 goal_num_ite n s1 s2 =
   do s <- get
@@ -954,6 +973,7 @@ provePrim script t = do
              , goalLoc  = show pos
              , goalDesc = ""
              , goalProp = prop
+             , goalTags = mempty
              }
   res <- SV.runProofScript script goal Nothing "prove_prim"
   case res of
@@ -979,6 +999,7 @@ proveHelper nm script t f = do
              , goalLoc  = show pos
              , goalDesc = ""
              , goalProp = prop
+             , goalTags = mempty
              }
   opts <- rwPPOpts <$> getTopLevelRW
   res <- SV.runProofScript script goal Nothing (Text.pack nm)
@@ -1024,6 +1045,7 @@ satPrim script t =
                 , goalLoc  = show pos
                 , goalDesc = ""
                 , goalProp = prop
+                , goalTags = mempty
                 }
      res <- SV.runProofScript script goal Nothing "sat"
      case res of
@@ -1504,6 +1526,7 @@ prove_core script input =
                 , goalLoc  = show pos
                 , goalDesc = ""
                 , goalProp = p
+                , goalTags = mempty
                 }
      res <- SV.runProofScript script goal Nothing "prove_core"
      let failProof pst =

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -279,15 +279,23 @@ type GhostGlobal = Crucible.GlobalVar GhostType
 --------------------------------------------------------------------------------
 -- ** Pre- and post-conditions
 
+data ConditionMetadata =
+  ConditionMetadata
+  { conditionLoc  :: ProgramLoc
+  , conditionTags :: Set String
+  , conditionType :: String
+  , conditionContext :: String
+  }
+ deriving (Show, Eq, Ord)
 
 --------------------------------------------------------------------------------
 -- *** StateSpec
 
 data SetupCondition ext where
-  SetupCond_Equal    :: ProgramLoc -> SetupValue ext -> SetupValue ext -> SetupCondition ext
-  SetupCond_Pred     :: ProgramLoc -> TypedTerm -> SetupCondition ext
+  SetupCond_Equal    :: ConditionMetadata -> SetupValue ext -> SetupValue ext -> SetupCondition ext
+  SetupCond_Pred     :: ConditionMetadata -> TypedTerm -> SetupCondition ext
   SetupCond_Ghost    :: B (HasGhostState ext) ->
-                        ProgramLoc ->
+                        ConditionMetadata ->
                         GhostGlobal ->
                         TypedTerm ->
                         SetupCondition ext