uc-crux-llvm: User-provided specifications for functions

crucible-syntax/test-data/simulator-tests/override-nondet-test-0.cbl

@@ -0,0 +1,8 @@
+(defun @main () Integer
+  (start start:
+    (let x (fresh Integer))
+    (let y (fresh Integer))
+    (let z (funcall @nondetBranchesTest 0 x y))
+    (assert! (equal? z x) "should be true!")
+    (return z))
+)

crucible-syntax/test-data/simulator-tests/override-nondet-test-0.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====

crucible-syntax/test-data/simulator-tests/override-nondet-test-1.cbl

@@ -0,0 +1,8 @@
+(defun @main () Integer
+  (start start:
+    (let x (fresh Integer))
+    (let y (fresh Integer))
+    (let z (funcall @nondetBranchesTest 1 x y))
+    (assert! (equal? z y) "should be true!")
+    (return z))
+)

crucible-syntax/test-data/simulator-tests/override-nondet-test-1.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====

crucible-syntax/test-data/simulator-tests/override-nondet-test-both.cbl

@@ -0,0 +1,11 @@
+(defun @main () Integer
+  (start start:
+    (let w (fresh Integer))
+    (let x (fresh Integer))
+    (let y (fresh Integer))
+    (assume! (or (equal? w 0) (equal? w 1)) "w is 0 or 1")
+    (let z (funcall @nondetBranchesTest w x y))
+    (assert! (or (equal? z x) (equal? z y)) "should be true!")
+    (assert! (or (equal? x y) (not (and (equal? z x) (equal? z y)))) "should be true!")
+    (return z))
+)

crucible-syntax/test-data/simulator-tests/override-nondet-test-both.out.good

@@ -0,0 +1,72 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== Proof obligations ====
+Assuming:
+* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1
+    not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)))
+* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0
+    not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))
+* The branch in nondetBranchesTest from after branch 0 to after branch 1
+    not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i))
+* The branch in nondetBranchesTest from after branch 1 to default branch
+    let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v16 = eq 2 cnondetBranchesZ@11:i
+     in and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) v16
+Prove:
+  default branch: error: in nondetBranchesTest
+  fall-through branch
+  false
+PROVED
+Assuming:
+* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1
+    not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)))
+* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0
+    let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v7 = eq 0 cw@0:i
+        -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v12 = eq 0 cnondetBranchesZ@11:i
+     in not (and v7 v12 (not (and v7 v12)))
+* The branch in nondetBranchesTest from after branch 0 to second branch
+    let -- test-data/simulator-tests/override-nondet-test-both.cbl:10:5
+        v43 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i)))
+     in not v43
+* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to first branch
+    let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v7 = eq 0 cw@0:i
+        -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v12 = eq 0 cnondetBranchesZ@11:i
+     in not (and v7 v12 (not (and v7 v12)))
+Prove:
+  test-data/simulator-tests/override-nondet-test-both.cbl:8:5: error: in main
+  should be true!
+  let -- after branch 2
+      v28 = ite (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i)) cx@1:i cy@2:i
+   in not (and (not (eq v28 cx@1:i)) (not (eq v28 cy@2:i)))
+PROVED
+Assuming:
+* in main test-data/simulator-tests/override-nondet-test-both.cbl:6:5: w is 0 or 1
+    not (and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)))
+* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to after branch 0
+    let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v7 = eq 0 cw@0:i
+        -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v12 = eq 0 cnondetBranchesZ@11:i
+     in not (and v7 v12 (not (and v7 v12)))
+* The branch in nondetBranchesTest from after branch 0 to second branch
+    let -- test-data/simulator-tests/override-nondet-test-both.cbl:10:5
+        v54 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i)))
+     in not v54
+* The branch in main from test-data/simulator-tests/override-nondet-test-both.cbl:7:12 to first branch
+    let -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v7 = eq 0 cw@0:i
+        -- test-data/simulator-tests/override-nondet-test-both.cbl:7:12
+        v12 = eq 0 cnondetBranchesZ@11:i
+     in not (and v7 v12 (not (and v7 v12)))
+Prove:
+  test-data/simulator-tests/override-nondet-test-both.cbl:9:5: error: in main
+  should be true!
+  let -- after branch 2
+      v28 = ite (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i)) cx@1:i cy@2:i
+   in not (and (eq v28 cx@1:i) (eq v28 cy@2:i) (not (eq cx@1:i cy@2:i)))
+PROVED

crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.cbl

@@ -0,0 +1,9 @@
+(defun @main () Integer
+  (start start:
+    (let w (fresh Integer))
+    (let x (fresh Integer))
+    (let y (fresh Integer))
+    (assume! (and (not (equal? w 0)) (not (equal? w 1))) "w is not 0 or 1")
+    (let z (funcall @nondetBranchesTest w x y))
+    (return z))
+)

crucible-syntax/test-data/simulator-tests/override-nondet-test-neither.out.good

@@ -0,0 +1,20 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== Proof obligations ====
+Assuming:
+* in main test-data/simulator-tests/override-nondet-test-neither.cbl:6:5: w is not 0 or 1
+    and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i))
+* The branch in main from test-data/simulator-tests/override-nondet-test-neither.cbl:7:12 to after branch 0
+    not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@12:i))
+* The branch in nondetBranchesTest from after branch 0 to after branch 1
+    not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@12:i))
+* The branch in nondetBranchesTest from after branch 1 to default branch
+    let -- test-data/simulator-tests/override-nondet-test-neither.cbl:7:12
+        v17 = eq 2 cnondetBranchesZ@12:i
+     in and (not (eq 0 cw@0:i)) (not (eq 1 cw@0:i)) v17
+Prove:
+  default branch: error: in nondetBranchesTest
+  fall-through branch
+  false
+COUNTEREXAMPLE

crucible-syntax/test/Overrides.hs

@@ -39,7 +39,9 @@ setupOverrides _ ha =
                      <*> pure (UseOverride (mkOverride "symbolicBranchTest" symbolicBranchTest))
      f2 <- FnBinding <$> mkHandle ha "symbolicBranchesTest"
                      <*> pure (UseOverride (mkOverride "symbolicBranchesTest" symbolicBranchesTest))
-     return [(f1, InternalPos),(f2,InternalPos)]
+     f3 <- FnBinding <$> mkHandle ha "nondetBranchesTest"
+                     <*> pure (UseOverride (mkOverride "nondetBranchesTest" nondetBranchesTest))
+     return [(f1, InternalPos),(f2,InternalPos),(f3,InternalPos)]
 
 
 -- Test the @symbolicBranch@ override operation.
@@ -91,3 +93,26 @@ symbolicBranchesTest =
         liftIO $ intAdd sym y x2
 
   b4 = overrideError (GenericSimError "fall-through branch")
+
+
+-- Test the @nondetBranches@ override operation.
+--
+-- If the first argument is zero, returns the second argument. If it is one,
+-- returns the third argument. If it could be either, returns both (i.e.,
+-- nondeterministic choice). If it couldn't be either, errors out.
+nondetBranchesTest :: IsSymInterface sym =>
+  OverrideSim p sym ext r
+    (EmptyCtx ::> IntegerType ::> IntegerType ::> IntegerType) IntegerType (RegValue sym IntegerType)
+nondetBranchesTest =
+  do sym <- getSymInterface
+     args <- getOverrideArgs
+     cond <- reg @0 <$> getOverrideArgs
+     p1 <- liftIO $ intEq sym cond =<< intLit sym 0
+     p2 <- liftIO $ intEq sym cond =<< intLit sym 1
+     fallbackPred <- liftIO $ notPred sym =<< orPred sym p1 p2
+     let fallback = overrideError (GenericSimError "fall-through branch")
+     nondetBranches args
+       [ (p1, reg @1 <$> getOverrideArgs, Just (OtherPos "first branch"))
+       , (p2, reg @2 <$> getOverrideArgs, Just (OtherPos "second branch"))
+       , (fallbackPred, fallback, Just (OtherPos "default branch"))
+       ]

crucible/src/Lang/Crucible/Simulator/OverrideSim.hs

@@ -37,6 +37,7 @@ module Lang.Crucible.Simulator.OverrideSim
   , overrideAbort
   , symbolicBranch
   , symbolicBranches
+  , nondetBranches
   , overrideReturn
   , overrideReturn'
     -- * Function calls
@@ -86,6 +87,8 @@ import           Data.List (foldl')
 import qualified Data.Parameterized.Context as Ctx
 import           Data.Proxy
 import qualified Data.Text as T
+import           Data.Traversable (for)
+import           Numeric.Natural (Natural)
 import           System.Exit
 import           System.IO
 import           System.IO.Error
@@ -526,6 +529,9 @@ symbolicBranch p thn_args thn thn_pos els_args els els_pos =
 --   series of branches, one for each element of the list.  The semantics of
 --   this construct is that the predicates are evaluated in order, until
 --   the first one that evaluates true; this branch will be the taken branch.
+--   In other words, this operates like a chain of if-then-else statements;
+--   later branches assume that earlier branches were not taken.
+--
 --   If no predicate is true, the construct will abort with a @VariantOptionsExhausted@
 --   reason.  If you wish to report an error condition instead, you should add a
 --   final default case with a true predicate that calls @overrideError@.
@@ -555,6 +561,40 @@ symbolicBranches new_args xs0 =
               in overrideSymbolicBranch p all_args m' mpos old_args (go (i+1) xs) (Just (OtherPos msg))
        go (0::Integer) xs0
 
+-- | Non-deterministically choose among several feasible branches.
+--
+-- Unlike 'symbolicBranches', this function does not take only the first branch
+-- with a predicate that evaluates to true; instead it takes /all/ branches with
+-- predicates that are not syntactically false (or cannot be proved unreachable
+-- with path satisfiability checking, if enabled). Each branch will /not/ assume
+-- that other branches weren't taken.
+--
+-- As with 'symbolicBranch', any symbolic values needed by the branches should be
+-- placed into the @RegMap@ argument and retrieved when needed. See the comment
+-- on 'symbolicBranch'.
+--
+-- Operationally, this works by by numbering all of the branches from 0 to n,
+-- inventing a symbolic integer variable z, and adding z = i (where i ranges
+-- from 0 to n) to the branch condition for each branch, and calling
+-- 'symbolicBranches' on the result. Even though each branch given to
+-- 'symbolicBranches' assumes earlier branches are not taken, each branch
+-- condition has the form @(z = i) and p@, so the negation @~((z = i) and p)@
+-- is equivalent to @(z != i) or ~p@, so later branches don't assume the
+-- negation of the branch condition of earlier branches (i.e., @~p@).
+nondetBranches :: forall p sym ext rtp args new_args res a.
+  IsSymInterface sym =>
+  RegMap sym new_args {- ^ argument values for the branches -} ->
+  [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a, Maybe Position)]
+   {- ^ Branches to consider -} ->
+  OverrideSim p sym ext rtp args res a
+nondetBranches new_args xs0 =
+  do sym <- getSymInterface
+     z <- liftIO $ freshNat sym (safeSymbol "nondetBranchesZ")
+     xs <- for (zip [(0 :: Natural)..] xs0) $ \(i, (p, v, position)) ->
+       do p' <- liftIO $ andPred sym p =<< natEq sym z =<< natLit sym i
+          return (p', v, position)
+     symbolicBranches new_args xs
+
 --------------------------------------------------------------------------------
 -- FnBinding
 

uc-crux-llvm/.hlint.yaml

@@ -79,17 +79,23 @@
     name: "Use void"
     within:
       - "UCCrux.LLVM.View.Shape"
+- ignore:  # "SpecPreconds" should be extensible with more fields
+    name: "Use newtype instead of data"
+    within: ["UCCrux.LLVM.Specs.Type"]
 - ignore:  # False positive - Template Haskell
     name: "Redundant bracket"
     within:
       - "UCCrux.LLVM.Cursor"
       - "UCCrux.LLVM.FullType.FuncSig"
       - "UCCrux.LLVM.FullType.Type"
       - "UCCrux.LLVM.FullType.VarArgs"
+      - "UCCrux.LLVM.Newtypes.FunctionName"
       - "UCCrux.LLVM.Shape"
       - "UCCrux.LLVM.View.Constraint"
       - "UCCrux.LLVM.View.Cursor"
       - "UCCrux.LLVM.View.FullType"
       - "UCCrux.LLVM.View.Postcond"
+      - "UCCrux.LLVM.View.Precond"
       - "UCCrux.LLVM.View.Shape"
+      - "UCCrux.LLVM.View.Specs"
       - "UCCrux.LLVM.View.Util"

uc-crux-llvm/README.md

@@ -225,6 +225,10 @@ crash-equivalence is an equivalence relation. Use `--entry-points` to check
 specific functions, or `--explore` to check all functions from both programs
 that share a name.
 
+### Providing Specifications for External Functions
+
+See [./doc/specs.md](./doc/specs.md).
+
 ## Developer Documentation
 
 See [./doc/developing.md](./doc/developing.md).