AArch32: Support conditional returns (#243)

Adds support in macaw-aarch32 for conditional returns. These are not supported in core macaw, and are thus architecture-specific block terminators.

This required changes to the type of arch-specific block terminators. Before, `ArchTermStmt` was only parameterized by a state thread (`ids`).  This meant that they could not contain macaw (or crucible) values.  Some work on. AArch32 requires being able to store condition values in arch terminators (to support conditional returns). This change modifies the `ArchTermStmt` to enable this, which requires a bit of plumbing through various definitions and some extra instances.

In support of actually using this, it also became necessary to plumb fallthrough block labels through the architecture-specific terminator translation in macaw-symbolic.

Note that this change was overdue, as the PowerPC backend was storing macaw values in a way that would have rendered them unusable in the macaw-ppc-symbolic translation, had any interpretation been provided.  These new changes will enable a handler to be written for the conditional PowerPC trap instructions.

PowerPC, x86, and ARM have been updated.

Improves the macaw-aarch32 tests. There is now a command line option to save the generated macaw IR for each
discovered function to /tmp. Note that this reuses some infrastructure from the macaw-symbolic tests. This
shared functionality should be extracted into a macaw-testing library.

base/ChangeLog.md

@@ -0,0 +1,20 @@
+# Revision history for macaw-base
+
+## Next
+
+### Features
+
+### API Changes
+
+- Architecture-specific block terminators can now contain macaw values
+
+  This changed the type of the architecture extension block terminators from `ArchTermStmt ids` to `ArchTermStmt f` where `f ~ Value arch ids` at the macaw level.
+
+- Architecture backends can now configure the block classification during the discovery phase
+
+  The interface to configure block classification is exposed through the `ArchitectureInfo`. Note that clients that have not created their own `ArchitectureInfo` from scratch should be unaffected (which is the vast majority).
+
+- The post-discovery AST types are now exported from `Data.Macaw.Discovery.ParsedContents`
+
+  It is recommended that future references to these types be done through this module. They are re-exported from their original location (`Data.Macaw.Discovery.State`) for backwards compatibility. One day that is likely to change.
+

base/src/Data/Macaw/Analysis/FunctionArgs.hs

@@ -285,7 +285,7 @@ data ArchTermStmtRegEffects arch
 --
 -- The second is the state of registers when it is executed.
 type ComputeArchTermStmtEffects arch ids
-   = ArchTermStmt arch ids
+   = ArchTermStmt arch (Value arch ids)
    -> RegState (ArchReg arch) (Value arch ids)
    -> ArchTermStmtRegEffects arch
 

base/src/Data/Macaw/Analysis/RegisterUse.hs

@@ -1246,12 +1246,12 @@ type PostTermStmtInvariants arch ids =
   StartInferContext arch
   -> InferState arch ids
   -> Int
-  -> ArchTermStmt arch ids
+  -> ArchTermStmt arch (Value arch ids)
   -> RegState (ArchReg arch) (Value arch ids)
   -> Either (RegisterUseError arch) (PostValueMap arch ids, BlockStartConstraints arch)
 
 type ArchTermStmtUsageFn arch ids
-  = ArchTermStmt arch ids
+  = ArchTermStmt arch (Value arch ids)
   -> RegState (ArchReg arch) (Value arch ids)
   -> BlockUsageSummary arch ids
   -> Either (RegisterUseError arch) (RegDependencyMap arch ids)

base/src/Data/Macaw/Architecture/Info.hs

@@ -317,8 +317,8 @@ data ArchitectureInfo arch
                            .  ArchStmt arch (Value arch src)
                            -> Rewriter arch s src tgt ())
        -- ^ This rewrites an architecture specific statement
-     , rewriteArchTermStmt :: (forall s src tgt . ArchTermStmt arch src
-                                             -> Rewriter arch s src tgt (ArchTermStmt arch tgt))
+     , rewriteArchTermStmt :: (forall s src tgt . ArchTermStmt arch (Value arch src)
+                                             -> Rewriter arch s src tgt (ArchTermStmt arch (Value arch tgt)))
        -- ^ This rewrites an architecture specific statement
      , archDemandContext :: !(DemandContext arch)
        -- ^ Provides architecture-specific information for computing which arguments must be
@@ -331,7 +331,7 @@ data ArchitectureInfo arch
                                      -> Jmp.IntraJumpBounds arch ids
                                      -> RegState (ArchReg arch) (Value arch ids)
                                         -- The architecture-specific statement
-                                     -> ArchTermStmt arch ids
+                                     -> ArchTermStmt arch (Value arch ids)
                                      -> Maybe (Jmp.IntraJumpTarget arch))
        -- ^ This takes an abstract state from before executing an abs
        -- state, and an architecture-specific terminal statement.

base/src/Data/Macaw/CFG/AssignRhs.hs

@@ -76,14 +76,11 @@ type family ArchStmt (arch :: Kind.Type) = (stmt :: (Type -> Kind.Type) -> Kind.
 -- | A type family for defining architecture-specific statements that
 -- may have instruction-specific effects on control-flow and register state.
 --
--- The second type parameter is the ids phantom type used to provide
--- uniqueness of Nonce values that identify assignments.
---
 -- An architecture-specific terminal statement may have side effects and change register
--- values, it may or may not return to the current function.  If it does return to the
--- current function, it is assumed to be at most one location, and the block-translator
--- must provide that value at translation time.
-type family ArchTermStmt (arch :: Kind.Type) :: Kind.Type -> Kind.Type
+-- values, it may or may not return to the current function.
+--
+-- Note that the meaning of the type parameter is identical to that of 'ArchStmt'
+type family ArchTermStmt (arch :: Kind.Type) :: (Type -> Kind.Type) -> Kind.Type
    -- NOTE: Not injective because PPC32 and PPC64 use the same type.
 
 -- | Number of bits in addreses for architecture.

base/src/Data/Macaw/CFG/Block.hs

@@ -40,7 +40,7 @@ data TermStmt arch ids
     --
     -- The registers include the state of registers just before the terminal statement
     -- executes.
-  | ArchTermStmt !(ArchTermStmt arch ids)
+  | ArchTermStmt !(ArchTermStmt arch (Value arch ids))
                  !(RegState (ArchReg arch) (Value arch ids))
 
 instance ArchConstraints arch
@@ -55,7 +55,7 @@ instance ArchConstraints arch
     , indent 2 (pretty s) ]
   pretty (ArchTermStmt ts regs) =
     vcat
-    [ prettyF ts
+    [ ppArchTermStmt pretty ts
     , indent 2 (pretty regs) ]
 
 ------------------------------------------------------------------------

base/src/Data/Macaw/CFG/Core.hs

@@ -74,6 +74,7 @@ module Data.Macaw.CFG.Core
   , PrettyRegValue(..)
   , IsArchFn(..)
   , IsArchStmt(..)
+  , IsArchTermStmt(..)
   , collectValueRep
   , ppValueAssignments'
   , DocF
@@ -736,14 +737,20 @@ class IsArchStmt (f :: (Type -> Kind.Type) -> Kind.Type)  where
              -> f v
              -> Doc ann
 
+class IsArchTermStmt (f :: (Type -> Kind.Type) -> Kind.Type) where
+  ppArchTermStmt :: (forall u . v u -> Doc ann)
+                 -- ^ Function to pretty print contained values
+                 -> f v
+                 -> Doc ann
+
 -- | Constructs expected by architectures type classes.
 type ArchConstraints arch
    = ( RegisterInfo (ArchReg arch)
      , FoldableFC (ArchFn arch)
      , IsArchFn   (ArchFn arch)
      , IsArchStmt (ArchStmt arch)
      , FoldableF  (ArchStmt arch)
-     , PrettyF    (ArchTermStmt arch)
+     , IsArchTermStmt (ArchTermStmt arch)
      , IPAlignment arch
      )
 

base/src/Data/Macaw/Discovery/Classifier.hs

@@ -26,6 +26,8 @@ module Data.Macaw.Discovery.Classifier (
   , directJumpClassifier
   , noreturnCallClassifier
   , tailCallClassifier
+  -- * Reusable helpers
+  , branchBlockState
   ) where
 
 import           Control.Applicative ( Alternative(empty) )

base/src/Data/Macaw/Discovery/ParsedContents.hs

@@ -216,7 +216,7 @@ data ParsedTermStmt arch ids
   | ParsedReturn !(RegState (ArchReg arch) (Value arch ids))
   -- | An architecture-specific statement with the registers prior to execution, and
   -- the given next control flow address.
-  | ParsedArchTermStmt !(ArchTermStmt arch ids)
+  | ParsedArchTermStmt !(ArchTermStmt arch (Value arch ids))
                        !(RegState (ArchReg arch) (Value arch ids))
                        !(Maybe (ArchSegmentOff arch))
   -- | An error occured in translating the block
@@ -262,7 +262,7 @@ ppTermStmt tstmt =
       , PP.indent 2 (PP.pretty s) ]
     ParsedArchTermStmt ts s maddr ->
       PP.vcat
-      [ prettyF ts <> addrDoc
+      [ ppArchTermStmt PP.pretty ts <> addrDoc
       , PP.indent 2 (PP.pretty s) ]
       where
           addrDoc = case maddr of

macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal

@@ -27,6 +27,7 @@ library
                        containers,
                        lens,
                        panic,
+                       text,
                        parameterized-utils,
                        asl-translator,
                        what4,

macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs

@@ -14,6 +14,7 @@ module Data.Macaw.AArch32.Symbolic (
   , updateReg
   ) where
 
+import qualified Data.Text as T
 import           GHC.TypeLits
 
 import           Control.Lens ( (&), (%~) )
@@ -32,6 +33,8 @@ import qualified Data.Parameterized.TraversableF as TF
 import qualified Data.Parameterized.TraversableFC as FC
 import           Data.Proxy ( Proxy(..) )
 import qualified What4.BaseTypes as WT
+import qualified What4.ProgramLoc as WP
+import qualified What4.Utils.StringLiteral as WUS
 import qualified What4.Symbol as WS
 
 import qualified Language.ASL.Globals as LAG
@@ -41,6 +44,7 @@ import qualified Data.Macaw.ARM.ARMReg as MAR
 
 import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.CFG.Extension as CE
+import qualified Lang.Crucible.CFG.Expr as LCE
 import qualified Lang.Crucible.CFG.Reg as CR
 import qualified Lang.Crucible.Simulator.RegMap as MCR
 import qualified Lang.Crucible.Simulator.RegValue as MCRV
@@ -97,29 +101,28 @@ instance MS.GenArchInfo mem SA.AArch32 where
 data AArch32StmtExtension (f :: CT.CrucibleType -> Type) (ctp :: CT.CrucibleType) where
   AArch32PrimFn :: MAA.ARMPrimFn (AA.AtomWrapper f) t -> AArch32StmtExtension f (MS.ToCrucibleType t)
   AArch32PrimStmt :: MAA.ARMStmt (AA.AtomWrapper f) -> AArch32StmtExtension f CT.UnitType
-  AArch32PrimTerm :: MAA.ARMTermStmt ids -> AArch32StmtExtension f CT.UnitType
+  AArch32PrimTerm :: MAA.ARMTermStmt (AA.AtomWrapper f) -> AArch32StmtExtension f CT.UnitType
 
 instance FC.FunctorFC AArch32StmtExtension where
   fmapFC f st =
     case st of
       AArch32PrimFn p -> AArch32PrimFn (FC.fmapFC (AA.liftAtomMap f) p)
       AArch32PrimStmt p -> AArch32PrimStmt (TF.fmapF (AA.liftAtomMap f) p)
-      AArch32PrimTerm p -> AArch32PrimTerm p
+      AArch32PrimTerm p -> AArch32PrimTerm (TF.fmapF (AA.liftAtomMap f) p)
 
 instance FC.FoldableFC AArch32StmtExtension where
   foldMapFC f st =
     case st of
       AArch32PrimFn p -> FC.foldMapFC (AA.liftAtomIn f) p
       AArch32PrimStmt p -> TF.foldMapF (AA.liftAtomIn f) p
-      -- There is no data in terminators for now, so we can have a trivial implementation
-      AArch32PrimTerm _p -> mempty
+      AArch32PrimTerm p -> TF.foldMapF (AA.liftAtomIn f) p
 
 instance FC.TraversableFC AArch32StmtExtension where
   traverseFC f st =
     case st of
       AArch32PrimFn p -> AArch32PrimFn <$> FC.traverseFC (AA.liftAtomTrav f) p
       AArch32PrimStmt p -> AArch32PrimStmt <$> TF.traverseF (AA.liftAtomTrav f) p
-      AArch32PrimTerm p -> pure (AArch32PrimTerm p)
+      AArch32PrimTerm p -> AArch32PrimTerm <$> TF.traverseF (AA.liftAtomTrav f) p
 
 instance CE.TypeApp AArch32StmtExtension where
   appType st =
@@ -135,7 +138,7 @@ instance CE.PrettyApp AArch32StmtExtension where
         I.runIdentity (MC.ppArchFn (I.Identity . AA.liftAtomIn ppSub) p)
       AArch32PrimStmt p ->
         MC.ppArchStmt (AA.liftAtomIn ppSub) p
-      AArch32PrimTerm p -> MC.prettyF p
+      AArch32PrimTerm p -> MC.ppArchTermStmt (AA.liftAtomIn ppSub) p
 
 type instance MSB.MacawArchStmtExtension SA.AArch32 =
   AArch32StmtExtension
@@ -191,11 +194,40 @@ aarch32GenStmt s = do
   s' <- TF.traverseF f s
   void (MSB.evalArchStmt (AArch32PrimStmt s'))
 
-aarch32GenTermStmt :: MAA.ARMTermStmt ids
+aarch32GenTermStmt :: MAA.ARMTermStmt (MC.Value SA.AArch32 ids)
                    -> MC.RegState MAR.ARMReg (MC.Value SA.AArch32 ids)
+                   -> Maybe (CR.Label s)
                    -> MSB.CrucGen SA.AArch32 ids s ()
-aarch32GenTermStmt ts _regs =
-  void (MSB.evalArchStmt (AArch32PrimTerm ts))
+aarch32GenTermStmt ts regs mfallthroughLabel =
+  case ts of
+    MAA.ReturnIf cond -> returnIf =<< MSB.valueToCrucible cond
+    MAA.ReturnIfNot cond -> do
+      notc <- MSB.appAtom =<< LCE.Not <$> MSB.valueToCrucible cond
+      returnIf notc
+    _ -> do
+      ts' <- TF.traverseF f ts
+      void (MSB.evalArchStmt (AArch32PrimTerm ts'))
+  where
+    f x = AA.AtomWrapper <$> MSB.valueToCrucible x
+    returnIf cond = do
+      MSB.setMachineRegs =<< MSB.createRegStruct regs
+      tlbl <- CR.Label <$> MSB.freshValueIndex
+      flbl <- case mfallthroughLabel of
+        Just ft -> return ft
+        Nothing -> do
+          ft <- CR.Label <$> MSB.freshValueIndex
+          errMsg <- MSB.evalAtom (CR.EvalApp (LCE.StringLit (WUS.UnicodeLiteral (T.pack "No fallthrough for conditional return"))))
+          let err = CR.ErrorStmt errMsg
+          let eblock = CR.mkBlock (CR.LabelID ft) mempty mempty (WP.Posd WP.InternalPos err)
+          MSB.addExtraBlock eblock
+          return ft
+
+      regValues <- MSB.createRegStruct regs
+      let ret = CR.Return regValues
+      let rblock = CR.mkBlock (CR.LabelID tlbl) mempty mempty (WP.Posd WP.InternalPos ret)
+      MSB.addExtraBlock rblock
+
+      MSB.addTermStmt $! CR.Br cond tlbl flbl
 
 regIndexMap :: MSB.RegIndexMap SA.AArch32
 regIndexMap = MSB.mkRegIndexMap asgn sz

macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/Functions.hs

@@ -80,6 +80,8 @@ termSemantics _sfns tstmt _st0 =
       X.throwIO UnsupportedSyscall
     MAA.ThumbSyscall _payload ->
       X.throwIO UnsupportedSyscall
+    MAA.ReturnIf _cond -> AP.panic AP.AArch32 "termSemantics" ["ReturnIf should be translated away when lifting from macaw to crucible"]
+    MAA.ReturnIfNot _cond -> AP.panic AP.AArch32 "termSemantics" ["ReturnIfNot should be translated away when lifting from macaw to crucible"]
 
 -- | Semantics for statement syntax extensions
 --

macaw-aarch32-symbolic/tests/pass/Makefile

@@ -11,3 +11,9 @@ all: $(unopt) $(opt)
 
 %.opt.exe : %.c
 	$(CC) $(CFLAGS) -O2 $< -o $@
+
+# We have to use -O1 for this case; -O0 won't generate a conditional return,
+# while -O2 generates some totally different code where the compiler just
+# conditionally performs a bunch of other operations instead
+test-conditional-return.opt.exe: test-conditional-return.c
+	$(CC) $(CFLAGS) -O1 $< -o $@

macaw-aarch32-symbolic/tests/pass/test-conditional-return.c

@@ -0,0 +1,24 @@
+#include "util.h"
+
+int g = -11;
+
+int __attribute__((noinline)) test_conditional_return(int x, int y, int z) {
+  // Note that this early return is entirely in terms of `x` because we are
+  // trying to convince the compiler to generate a conditional return. If there
+  // is too much here (e.g., register moves), it generally won't do it. Since
+  // `x` is in r0 (and the return value is in r0), this usually convinces the
+  // compiler to generate the necessary code.
+  if(x > 0) return x;
+
+  g = g + 1;
+  g = g - y + x;
+  int ret = y;
+  if(ret <= 0) ret = 1;
+
+  return ret;
+}
+
+void _start() {
+  test_conditional_return(1, g, 0);
+  EXIT();
+}

macaw-aarch32-symbolic/tests/pass/util.h

@@ -0,0 +1,3 @@
+#define EXIT() \
+  asm("mov     %r7, $1");  \
+  asm("svc #0")

macaw-aarch32/macaw-aarch32.cabal

@@ -20,6 +20,7 @@ library
                      , Data.Macaw.ARM.Disassemble
                      , Data.Macaw.ARM.Eval
                      , Data.Macaw.ARM.Identify
+                     , Data.Macaw.ARM.Panic
                      , Data.Macaw.ARM.Semantics.ARMSemantics
                      , Data.Macaw.ARM.Semantics.ThumbSemantics
                      , Data.Macaw.ARM.Semantics.TH
@@ -40,6 +41,7 @@ library
                      , macaw-base
                      , macaw-semmc
                      , mtl
+                     , panic
                      , parameterized-utils
                      , pretty
                      , prettyprinter >= 1.7.0

macaw-aarch32/src/Data/Macaw/ARM.hs

@@ -11,10 +11,11 @@ module Data.Macaw.ARM
     )
     where
 
+import           Control.Applicative ( (<|>) )
 import           Data.Macaw.ARM.Arch
 import           Data.Macaw.ARM.Disassemble ( disassembleFn )
 import           Data.Macaw.ARM.Eval
-import           Data.Macaw.ARM.Identify ( identifyCall, identifyReturn, isReturnValue )
+import           Data.Macaw.ARM.Identify ( identifyCall, identifyReturn, isReturnValue, conditionalReturnClassifier )
 import qualified Data.Macaw.ARM.ARMReg as ARMReg
 import qualified Data.Macaw.ARM.Semantics.ARMSemantics as ARMSem
 import qualified Data.Macaw.ARM.Semantics.ThumbSemantics as ThumbSem
@@ -51,7 +52,7 @@ arm_linux_info =
                         , MI.rewriteArchTermStmt = rewriteTermStmt
                         , MI.archDemandContext = archDemandContext
                         , MI.postArchTermStmtAbsState = postARMTermStmtAbsState preserveRegAcrossSyscall
-                        , MI.archClassifier = MD.defaultClassifier
+                        , MI.archClassifier = conditionalReturnClassifier <|> MD.defaultClassifier
                         }
 
 archDemandContext :: MDS.DemandContext ARM.AArch32