change 'no-assume-stack-scope' to 'assume-stack-scope' and add docume…

…ntation

This flips the default behavior of this unsafe flag.

If set, 'assume-stack-scope' injects an additional
assumption into every pre-domain that all out of
scope stack values (i.e. past the stack pointer)

This is a fairly strong assumption that is unsafe in
general, in particular it will crash in the case where
it is provably false (i.e. the value domain implies that
the stack contents past the stack pointer are necessarily
inequivalent)

updates challenge10.args to use --assume-stack-scope

README.rst

@@ -87,8 +87,8 @@ The verifier accepts the following command line arguments::
   --read-only-segments ARG Mark segments as read-only (0-indexed) when loading
                            ELF
   --script FILENAME        Save macaw CFGs to the provided directory
-  --no-assume-stack-scope  Don't add additional assumptions about stack frame
-                           scoping
+  --assume-stack-scope     Add additional assumptions about stack frame scoping 
+                           during function calls (unsafe)
   --ignore-warnings ARG    Don't raise any of the given warning types
   --always-classify-return Always resolve classifier failures by assuming
                            function returns, if possible.

docs/user-manual/invoking.tex

@@ -88,11 +88,25 @@ \section{Invoking the \pate{} Verifier}
   --read-only-segments ARG Mark segments as read-only (0-indexed) when loading
                            ELF
   --script FILENAME        Save macaw CFGs to the provided directory
-  --no-assume-stack-scope  Don't add additional assumptions about stack frame
-                           scoping
+  --assume-stack-scope     Add additional assumptions about stack frame 
+                           scoping during function calls (unsafe)
   --ignore-warnings ARG    Don't raise any of the given warning types
 \end{verbatim}
 
+\subsection{--assume-stack-scope}
+
+This flag causes \pate{} to assume that out-of-scope stack slots 
+(i.e. slots that are past the current stack pointer) are always equal between
+the two binaries.
+Although in actuality they may have differing out-of-scope stack
+contents, programs that exercise proper stack hygiene should never
+access those values. By assuming they are equal, \pate{} avoids 
+creating spurious counter-examples where under-specified pointers
+alias inequivalent, but out-of-scope, stack slots.
+This is a fairly strong assumption that can have unintended side-effects,
+including assuming \emph{false} when out-of-scope stack contents are
+\emph{provably} inequivalent.
+
 
 %%% Local Variables:
 %%% mode: latex

src/Pate/CLI.hs

@@ -94,7 +94,7 @@ mkRunConfig archLoader opts rcfg mtt = let
         , PC.cfgRescopingFailureMode = rerrMode opts
         , PC.cfgScriptPath = scriptPath opts
         , PC.cfgTraceTree = fromMaybe noTraceTree mtt
-        , PC.cfgStackScopeAssume = not $ noAssumeStackScope opts
+        , PC.cfgStackScopeAssume = assumeStackScope opts
         , PC.cfgIgnoreWarnings = ignoreWarnings opts
         , PC.cfgAlwaysClassifyReturn = alwaysClassifyReturn opts
         , PC.cfgTraceConstraints = traceConstraints opts
@@ -147,7 +147,7 @@ data CLIOptions = CLIOptions
   , jsonToplevel :: Bool
   , readOnlySegments :: [Int]
   , scriptPath :: Maybe FilePath
-  , noAssumeStackScope :: Bool
+  , assumeStackScope :: Bool
   , ignoreWarnings :: [String]
   , alwaysClassifyReturn :: Bool
   , preferTextInput :: Bool
@@ -462,8 +462,8 @@ cliOptions = OA.info (OA.helper <*> parser)
          <> OA.help "Save macaw CFGs to the provided directory"
          ))
     <*> OA.switch
-         ( OA.long "no-assume-stack-scope"
-         <> OA.help "Don't add additional assumptions about stack frame scoping"
+         ( OA.long "assume-stack-scope"
+         <> OA.help "Add additional assumptions about stack frame scoping during function calls (unsafe)"
          )
     <*> OA.many (OA.strOption
         ( OA.long "ignore-warnings"

src/Pate/Config.hs

@@ -314,7 +314,7 @@ defaultVerificationCfg =
                      , cfgIgnoreDivergedControlFlow = False
                      , cfgTargetEquivRegs = []
                      , cfgRescopingFailureMode = ThrowOnEqRescopeFailure
-                     , cfgStackScopeAssume = True
+                     , cfgStackScopeAssume = False
                      , cfgScriptPath = Nothing
                      , cfgIgnoreWarnings = []
                      , cfgAlwaysClassifyReturn = False

tests/aarch32/scripted/challenge10.args

@@ -8,4 +8,5 @@
 -e ContinueAfterRecoverableFailures
 -r AllowEqRescopeFailure
 -s transport_handler
---script challenge10.pate
+--script challenge10.pate
+--assume-stack-scope

tests/template.mk

@@ -46,8 +46,7 @@ malloc-%.exe: ./build/malloc-%.s ./build/link.ld
 %.test_run: %.original.exe %.patched.exe
 	../../pate.sh -o $(basename $@).original.exe -p $(basename $@).patched.exe \
 		`( (test -f $(basename $@).toml && echo "-b $(basename $@).toml") || echo "")` \
-		`( (test -f $(basename $@).pate && echo "--script $(basename $@).pate") || echo "")` \
-		--no-assume-stack-scope
+		`( (test -f $(basename $@).pate && echo "--script $(basename $@).pate") || echo "")`
 
 .PRECIOUS: ./build/%.s ./build/%.i %.exe malloc-%.exe ./unequal/%.original.exe ./unequal/%.patched.exe