aarch32: Implement support for conditional calls (#289)

The core of macaw cannot represent conditional calls because the existing block terminators are not sufficiently expressive and it doesn't support creating synthetic blocks to represent control flow not directly tied to machine addresses.

To work around this, we introduce ARM-specific block terminators for conditional calls and plumb them through up to macaw-aarch32-symbolic.

Fixes #288

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

@@ -28,6 +28,7 @@ library
                        lens,
                        panic,
                        text,
+                       mtl,
                        parameterized-utils,
                        asl-translator,
                        what4,

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

@@ -1,11 +1,12 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Data.Macaw.AArch32.Symbolic (
@@ -15,11 +16,13 @@ module Data.Macaw.AArch32.Symbolic (
   ) where
 
 import qualified Data.Text as T
+import           GHC.Stack ( HasCallStack )
 import           GHC.TypeLits
 
 import           Control.Lens ( (&), (%~) )
 import           Control.Monad ( void )
 import           Control.Monad.IO.Class ( liftIO )
+import qualified Control.Monad.State as CMS
 import qualified Data.Functor.Identity as I
 import           Data.Kind ( Type )
 import qualified Data.Macaw.CFG as MC
@@ -34,6 +37,7 @@ import qualified Data.Parameterized.NatRepr as PN
 import qualified Data.Parameterized.TraversableF as TF
 import qualified Data.Parameterized.TraversableFC as FC
 import           Data.Proxy ( Proxy(..) )
+import qualified Data.Sequence as Seq
 import qualified What4.BaseTypes as WT
 import qualified What4.ProgramLoc as WP
 import qualified What4.Symbol as WS
@@ -210,6 +214,40 @@ aarch32GenStmt s = do
   s' <- TF.traverseF f s
   void (MSB.evalArchStmt (AArch32PrimStmt s'))
 
+-- | Create labels for a conditional branch in a Crucible statement handler
+--
+-- Create two labels (returned in order): the True label (to take when a
+-- condition evaluates to true during symbolic execution) and the False label
+-- (to fall through to otherwise)
+--
+-- This function requires that the fallthrough label exists; if we don't have
+-- one at translation time, make a fresh block that ends in an error.
+--
+-- Note that this lets us fail lazily (i.e., during symbolic execution and not
+-- translation time), as this non-existence only matters if we reach this part
+-- of the program during symbolic execution.
+makeConditionalLabels
+  :: (FC.TraversableFC (MSB.MacawArchStmtExtension arch))
+  => Maybe (CR.Label s)
+  -- ^ The fallthrough label
+  -> String
+  -- ^ A message to embed in case there is no fallthrough label and the block is
+  -- reached during symbolic execution
+  -> MSB.CrucGen arch ids s (CR.Label s, CR.Label s)
+makeConditionalLabels mfallthroughLabel msg = do
+  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 msg))))
+      let err = CR.ErrorStmt errMsg
+      let eblock = CR.mkBlock (CR.LabelID ft) mempty mempty (WP.Posd WP.InternalPos err)
+      MSB.addExtraBlock eblock
+      return ft
+  return (tlbl, flbl)
+
+
 aarch32GenTermStmt :: MAA.ARMTermStmt (MC.Value SA.AArch32 ids)
                    -> MC.RegState MAR.ARMReg (MC.Value SA.AArch32 ids)
                    -> Maybe (CR.Label s)
@@ -220,19 +258,21 @@ aarch32GenTermStmt ts regs mfallthroughLabel =
     MAA.ReturnIfNot cond -> do
       notc <- MSB.appAtom =<< LCE.Not <$> MSB.valueToCrucible cond
       returnIf notc
+    MAA.CallIf cond pc lr -> do
+      cond' <- MSB.valueToCrucible cond
+      pc' <- MSB.valueToCrucible pc
+      lr' <- MSB.valueToCrucible lr
+      callIf cond' pc' lr'
+    MAA.CallIfNot cond pc lr -> do
+      cond' <- MSB.valueToCrucible cond
+      pc' <- MSB.valueToCrucible pc
+      lr' <- MSB.valueToCrucible lr
+      notc <- MSB.appAtom (LCE.Not cond')
+      callIf notc pc' lr'
   where
     returnIf cond = do
       MSB.setMachineRegs =<< MSB.createRegStruct regs
-      tlbl <- CR.Label <$> MSB.freshValueIndex
+      (tlbl, flbl) <- makeConditionalLabels mfallthroughLabel "No fallthrough for conditional return"
-      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
@@ -241,20 +281,84 @@ aarch32GenTermStmt ts regs mfallthroughLabel =
 
       MSB.addTermStmt $! CR.Br cond tlbl flbl
 
+    -- Implement the semantics of conditional calls in Crucible
+    --
+    -- Note that we avoid generating Crucible IR with the 'MSB.CrucGen' monad
+    -- here because that adds code to the *current* block. We need to create
+    -- extra blocks here to model the necessary control flow.
+    callIf cond pc lr = do
+
+      -- First, create two labels: the True label (to take when @cond@ is true
+      -- during symbolic execution) and the False label (to fall through to
+      -- otherwise)
+      (tlbl, flbl) <- makeConditionalLabels mfallthroughLabel "No fallthrough for conditional call"
+
+      archFns <- CMS.gets MSB.translateFns
+      regsReg <- CMS.gets MSB.crucRegisterReg
+      let tps = MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr $ MS.crucGenRegAssignment archFns
+      let regsType = CT.StructRepr tps
+
+      -- Next, make a block to issue the call. We need to snapshot the register
+      -- state, pass it to the function handle lookup, then pass the snapshot
+      -- state to the actual function call, and then finally put the state back.
+      --
+      -- Note that we need to poke in the actual PC and LR values that are
+      -- active when we take the conditional call.  In the natural register
+      -- state at this point, the PC and LR contain muxes, with the actual
+      -- values taken depending on what the condition evaluates to. They are
+      -- correct as muxes, but if we leave them as muxes, the function that
+      -- looks them up might not handle that well. Some clients do not handle
+      -- symbolic function pointers, even when they resolve to a trivially
+      -- concrete value under the path condition. To account for that, in the
+      -- case where the conditional call is taken, we poke in the resolved PC
+      -- and LR to strip off the mux. Note that they could still be symbolic.
+      fhAtom <- MSB.mkAtom (CT.FunctionHandleRepr (Ctx.singleton regsType) regsType)
+      initialRegsAtom <- MSB.mkAtom regsType
+      pcRegsAtom <- MSB.mkAtom regsType
+      lrRegsAtom <- MSB.mkAtom regsType
+      newRegsAtom <- MSB.mkAtom regsType
+
+      let pcIdx = MSB.crucibleIndex (indexForReg MC.ip_reg)
+      let lrIdx = MSB.crucibleIndex (indexForReg MAR.arm_LR)
+
+      let stmts = [ CR.DefineAtom initialRegsAtom $ CR.ReadReg regsReg
+                  , CR.DefineAtom pcRegsAtom $ CR.EvalApp $ LCE.SetStruct tps initialRegsAtom pcIdx pc
+                  , CR.DefineAtom lrRegsAtom $ CR.EvalApp $ LCE.SetStruct tps pcRegsAtom lrIdx lr
+                  , CR.DefineAtom fhAtom $ CR.EvalExt (MS.MacawLookupFunctionHandle (MS.crucArchRegTypes archFns) lrRegsAtom)
+                  , CR.DefineAtom newRegsAtom $ CR.Call fhAtom (Ctx.singleton lrRegsAtom) regsType
+                  , CR.SetReg regsReg newRegsAtom
+                  ]
+      let asInternal = WP.Posd WP.InternalPos
+      let callBlock = CR.mkBlock (CR.LabelID tlbl) mempty (Seq.fromList [ asInternal s | s <- stmts]) (WP.Posd WP.InternalPos (CR.Jump flbl))
+      MSB.addExtraBlock callBlock
+
+      -- Finally, jump to either the block with the call or the fallthrough
+      -- label to skip it
+      MSB.addTermStmt $! CR.Br cond tlbl flbl
+
+
 regIndexMap :: MSB.RegIndexMap SA.AArch32
 regIndexMap = MSB.mkRegIndexMap asgn sz
   where
     asgn = aarch32RegAssignment
     sz = Ctx.size (MS.typeCtxToCrucible (FC.fmapFC MT.typeRepr asgn))
 
-updateReg :: MAR.ARMReg tp
+indexForReg
+  :: (HasCallStack)
+  => MAR.ARMReg tp
+  -> MSB.IndexPair (MS.ArchRegContext SA.AArch32) tp
+indexForReg reg =
+  case MapF.lookup reg regIndexMap of
+    Nothing -> AP.panic AP.AArch32 "indexForReg" ["Missing register index mapping for register: " ++ show reg]
+    Just p -> p
+
+updateReg :: (HasCallStack)
+          => MAR.ARMReg tp
           -> (f (MS.ToCrucibleType tp) -> f (MS.ToCrucibleType tp))
           -> Ctx.Assignment f (MS.MacawCrucibleRegTypes SA.AArch32)
           -> Ctx.Assignment f (MS.MacawCrucibleRegTypes SA.AArch32)
 updateReg reg upd asgn =
-  case MapF.lookup reg regIndexMap of
+  asgn & MapF.ixF (MSB.crucibleIndex (indexForReg reg)) %~ upd
-    Just pair -> asgn & MapF.ixF (MSB.crucibleIndex pair) %~ upd
-    Nothing -> AP.panic AP.AArch32 "updateReg" ["Missing reg entry for register: " ++ show reg]
 
 aarch32UpdateReg :: MCR.RegEntry sym (MS.ArchRegStruct SA.AArch32)
                  -> MAR.ARMReg tp
@@ -263,13 +367,12 @@ aarch32UpdateReg :: MCR.RegEntry sym (MS.ArchRegStruct SA.AArch32)
 aarch32UpdateReg regs reg val =
   regs { MCR.regValue = updateReg reg (const (MCRV.RV val)) (MCR.regValue regs) }
 
-lookupReg :: MAR.ARMReg tp
+lookupReg :: (HasCallStack)
+          => MAR.ARMReg tp
           -> Ctx.Assignment f (MS.MacawCrucibleRegTypes SA.AArch32)
           -> f (MS.ToCrucibleType tp)
 lookupReg reg regs =
-  case MapF.lookup reg regIndexMap of
+  regs Ctx.! MSB.crucibleIndex (indexForReg reg)
-    Just pair -> regs Ctx.! MSB.crucibleIndex pair
-    Nothing -> AP.panic AP.AArch32 "lookupReg" ["Missing reg entry for register: " ++ show reg]
 
 aarch32LookupReg :: MCR.RegEntry sym (MS.ArchRegStruct SA.AArch32)
                  -> MAR.ARMReg tp

macaw-aarch32-symbolic/tests/pass/test-conditional-call.c_template

@@ -0,0 +1,46 @@
+#include "util.h"
+
+// Note that this file is not compiled by the test suite build system because we
+// can't easily convince the compiler to produce the machine code we need.  The
+// marked line below (the conditional call) shows morally what we want the code
+// to be, but we have to manually mangle the assembly to ensure we get the
+// conditional call.
+//
+// Compile with:
+//
+// >>> arm-linux-gnu-gcc -x C -S test-conditional-call.c_template -o test-conditional-call.s
+//
+// to generate an assembly file, then:
+//
+// 1. Insert `cmp r0, #0` before the call, and
+// 2. Change the call to `bleq`
+
+
+int g;
+
+void __attribute__((noinline)) callee(int x) {
+  if(x == 0)
+    g = 1;
+}
+
+int __attribute__((noinline)) test_conditional_call(int x) {
+  g = 100;
+  if(x == 0)
+    g = -5;
+
+  // This is the condition we want, but that we can't trust the compiler
+  // to turn into a predicated call instruction
+  //
+  // if(x == 0)
+    callee(x);
+
+  // We are modifying the call to be conditional (if x is 0), so this should
+  // always succeed if the conditional call semantics are correct.
+  return g > 0;
+}
+
+void _start() {
+  g = 0;
+  test_conditional_call(5);
+  EXIT();
+}

macaw-aarch32-symbolic/tests/pass/test-conditional-call.s

@@ -0,0 +1,121 @@
+	.arch armv7-a
+	.eabi_attribute 28, 1
+	.eabi_attribute 20, 1
+	.eabi_attribute 21, 1
+	.eabi_attribute 23, 3
+	.eabi_attribute 24, 1
+	.eabi_attribute 25, 1
+	.eabi_attribute 26, 2
+	.eabi_attribute 30, 6
+	.eabi_attribute 34, 1
+	.eabi_attribute 18, 4
+	.file	"test-conditional-call.c"
+	.text
+	.global	g
+	.bss
+	.align	2
+	.type	g, %object
+	.size	g, 4
+g:
+	.space	4
+	.text
+	.align	2
+	.global	callee
+	.arch armv7-a
+	.syntax unified
+	.arm
+	.fpu vfpv3-d16
+	.type	callee, %function
+callee:
+	@ args = 0, pretend = 0, frame = 8
+	@ frame_needed = 1, uses_anonymous_args = 0
+	@ link register save eliminated.
+	str	fp, [sp, #-4]!
+	add	fp, sp, #0
+	sub	sp, sp, #12
+	str	r0, [fp, #-8]
+	ldr	r3, [fp, #-8]
+	cmp	r3, #0
+	bne	.L3
+	movw	r3, #:lower16:g
+	movt	r3, #:upper16:g
+	mov	r2, #1
+	str	r2, [r3]
+.L3:
+	nop
+	add	sp, fp, #0
+	@ sp needed
+	ldr	fp, [sp], #4
+	bx	lr
+	.size	callee, .-callee
+	.align	2
+	.global	test_conditional_call
+	.syntax unified
+	.arm
+	.fpu vfpv3-d16
+	.type	test_conditional_call, %function
+test_conditional_call:
+	@ args = 0, pretend = 0, frame = 8
+	@ frame_needed = 1, uses_anonymous_args = 0
+	push	{fp, lr}
+	add	fp, sp, #4
+	sub	sp, sp, #8
+	str	r0, [fp, #-8]
+	movw	r3, #:lower16:g
+	movt	r3, #:upper16:g
+	mov	r2, #100
+	str	r2, [r3]
+	ldr	r3, [fp, #-8]
+	cmp	r3, #0
+	bne	.L5
+	movw	r3, #:lower16:g
+	movt	r3, #:upper16:g
+	mvn	r2, #4
+	str	r2, [r3]
+.L5:
+	ldr	r0, [fp, #-8]
+  cmp r0, #0
+	bleq	callee
+	movw	r3, #:lower16:g
+	movt	r3, #:upper16:g
+	ldr	r3, [r3]
+	cmp	r3, #0
+	movgt	r3, #1
+	movle	r3, #0
+	uxtb	r3, r3
+	mov	r0, r3
+	sub	sp, fp, #4
+	@ sp needed
+	pop	{fp, pc}
+	.size	test_conditional_call, .-test_conditional_call
+	.align	2
+	.global	_start
+	.syntax unified
+	.arm
+	.fpu vfpv3-d16
+	.type	_start, %function
+_start:
+	@ args = 0, pretend = 0, frame = 0
+	@ frame_needed = 1, uses_anonymous_args = 0
+	push	{fp, lr}
+	add	fp, sp, #4
+	movw	r3, #:lower16:g
+	movt	r3, #:upper16:g
+	mov	r2, #0
+	str	r2, [r3]
+	mov	r0, #5
+	bl	test_conditional_call
+	.syntax divided
+@ 26 "test-conditional-call.c" 1
+	mov     %r7, $1
+@ 0 "" 2
+@ 26 "test-conditional-call.c" 1
+	svc #0
+@ 0 "" 2
+	.arm
+	.syntax unified
+	nop
+	pop	{fp, pc}
+	.size	_start, .-_start
+	.ident	"GCC: (GNU) 11.2.1 20210728 (Red Hat Cross 11.2.1-1)"
+	.section	.note.GNU-stack,"",%progbits

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

@@ -15,7 +15,7 @@ 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, conditionalReturnClassifier )
+import           Data.Macaw.ARM.Identify ( identifyCall, identifyReturn, isReturnValue, conditionalReturnClassifier, conditionalCallClassifier )
 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
@@ -52,7 +52,7 @@ arm_linux_info =
                         , MI.rewriteArchTermStmt = rewriteTermStmt
                         , MI.archDemandContext = archDemandContext
                         , MI.postArchTermStmtAbsState = postARMTermStmtAbsState preserveRegAcrossSyscall
-                        , MI.archClassifier = conditionalReturnClassifier <|> MD.defaultClassifier
+                        , MI.archClassifier = conditionalCallClassifier <|> conditionalReturnClassifier <|> MD.defaultClassifier
                         }
 
 archDemandContext :: MDS.DemandContext ARM.AArch32

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

@@ -113,6 +113,19 @@ data ARMTermStmt f where
   -- which requires a nonce). We work around this by just having an additional
   -- block terminator.
   ReturnIfNot :: f MT.BoolType -> ARMTermStmt f
+  -- | Conditional calls, with the same rationale as the conditional returns. The operands are:
+  --
+  --  * Condition
+  --
+  --  * Call target
+  --
+  --  * Return address
+  --
+  -- We need to extract the PC and LR values without the mux structure so that
+  -- we can poke it into the register state during symbolic execution
+  CallIf :: f MT.BoolType -> f (MT.BVType 32) -> f (MT.BVType 32) -> ARMTermStmt f
+  -- | Same as 'CallIf', but take the call if the condition is false instead
+  CallIfNot :: f MT.BoolType -> f (MT.BVType 32) -> f (MT.BVType 32) -> ARMTermStmt f
 
 instance Show (ARMTermStmt (MC.Value ARM.AArch32 ids)) where
   show ts = show (MC.ppArchTermStmt PP.pretty ts)
@@ -124,6 +137,8 @@ instance MC.IsArchTermStmt ARMTermStmt where
     case ts of
       ReturnIf cond -> "return_if" PP.<+> ppValue cond
       ReturnIfNot cond -> "return_if_not" PP.<+> ppValue cond
+      CallIf cond pc lr -> "call_if" PP.<+> ppValue cond PP.<+> "pc=" <> ppValue pc PP.<+> "lr=" <> ppValue lr
+      CallIfNot cond pc lr -> "call_if_not" PP.<+> ppValue cond PP.<+> "pc=" <> ppValue pc PP.<+> "lr=" <> ppValue lr
 
 instance TF.FoldableF ARMTermStmt where
   foldMapF = TF.foldMapFDefault
@@ -136,12 +151,16 @@ instance TF.TraversableF ARMTermStmt where
     case tstmt of
       ReturnIf cond -> ReturnIf <$> go cond
       ReturnIfNot cond -> ReturnIfNot <$> go cond
+      CallIf cond pc lr -> CallIf <$> go cond <*> go pc <*> go lr
+      CallIfNot cond pc lr -> CallIfNot <$> go cond <*> go pc <*> go lr
 
 rewriteTermStmt :: ARMTermStmt (MC.Value ARM.AArch32 src) -> Rewriter ARM.AArch32 s src tgt (ARMTermStmt (MC.Value ARM.AArch32 tgt))
 rewriteTermStmt s =
     case s of
       ReturnIf cond -> ReturnIf <$> rewriteValue cond
       ReturnIfNot cond -> ReturnIfNot <$> rewriteValue cond
+      CallIf cond pc lr -> CallIf <$> rewriteValue cond <*> rewriteValue pc <*> rewriteValue lr
+      CallIfNot cond pc lr -> CallIfNot <$> rewriteValue cond <*> rewriteValue pc <*> rewriteValue lr
 
 -- ----------------------------------------------------------------------
 -- ARM functions.  These may return a value, and may depend on the

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

@@ -35,6 +35,7 @@ import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.NatRepr (knownNat, NatRepr)
 import           Data.Parameterized.Some ( Some(..) )
 import qualified Data.Set as Set
+import           GHC.Stack ( HasCallStack )
 
 import qualified Language.ASL.Globals as ASL
 import qualified SemMC.Architecture.AArch32 as ARM
@@ -190,8 +191,35 @@ absEvalArchStmt :: MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids
                 -> MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids
 absEvalArchStmt s _ = s
 
+-- | Update the abstract state as if control flow had fallen through to the next
+-- instruction (i.e., if the conditional instruction is not taken). This is not
+-- semantically exact, but it is the right behavior to guide code discovery to
+-- the remaining code.
+--
+-- FIXME: This function uniformly increments the PC by 4 to compute the next
+-- PC. That is not necessarily correct for Thumb.
+abstractFallthrough
+  :: (HasCallStack)
+  => (forall tp . AR.ARMReg tp -> Bool)
+  -> MM.Memory 32
+  -> MA.AbsProcessorState AR.ARMReg ids
+  -> MJ.IntraJumpBounds ARM.AArch32 ids
+  -> MC.RegState AR.ARMReg (MC.Value ARM.AArch32 ids)
+  -> String
+  -> Maybe (MM.MemSegmentOff 32, MA.AbsBlockState AR.ARMReg, MJ.InitJumpBounds ARM.AArch32)
+abstractFallthrough preservePred mem s0 jumpBounds regState stmtName =
+  case simplifyValue (regState ^. MC.curIP) of
+    Just (MC.RelocatableValue _ addr)
+      | Just nextPC <- MM.asSegmentOff mem (MM.incAddr 4 addr) -> do
+          let params = MA.CallParams { MA.postCallStackDelta = 0
+                                     , MA.preserveReg = preservePred
+                                     , MA.stackGrowsDown = True
+                                     }
+          Just (nextPC, MA.absEvalCall params s0 regState nextPC, MJ.postCallBounds params jumpBounds regState)
+    _ -> MAP.panic MAP.AArch32Eval "postARMTermStmtAbsState" [stmtName ++ " could not interpret next PC: " ++ show (regState ^. MC.curIP)]
 
-postARMTermStmtAbsState :: (forall tp . AR.ARMReg tp -> Bool)
+postARMTermStmtAbsState :: (HasCallStack)
+                        => (forall tp . AR.ARMReg tp -> Bool)
                         -> MM.Memory 32
                         -> MA.AbsProcessorState AR.ARMReg ids
                         -> MJ.IntraJumpBounds ARM.AArch32 ids
@@ -200,26 +228,10 @@ postARMTermStmtAbsState :: (forall tp . AR.ARMReg tp -> Bool)
                         -> Maybe (MM.MemSegmentOff 32, MA.AbsBlockState AR.ARMReg, MJ.InitJumpBounds ARM.AArch32)
 postARMTermStmtAbsState preservePred mem s0 jumpBounds regState stmt =
   case stmt of
-    AA.ReturnIf _ ->
+    AA.ReturnIf _ -> abstractFallthrough preservePred mem s0 jumpBounds regState "ReturnIf"
-      case simplifyValue (regState ^. MC.curIP) of
+    AA.ReturnIfNot _ -> abstractFallthrough preservePred mem s0 jumpBounds regState "ReturnIfNot"
-        Just (MC.RelocatableValue _ addr)
+    AA.CallIf {} -> abstractFallthrough preservePred mem s0 jumpBounds regState "CallIf"
-          | Just nextPC <- MM.asSegmentOff mem (MM.incAddr 4 addr) -> do
+    AA.CallIfNot {} -> abstractFallthrough preservePred mem s0 jumpBounds regState "CallIfNot"
-              let params = MA.CallParams { MA.postCallStackDelta = 0
-                                         , MA.preserveReg = preservePred
-                                         , MA.stackGrowsDown = True
-                                         }
-              Just (nextPC, MA.absEvalCall params s0 regState nextPC, MJ.postCallBounds params jumpBounds regState)
-        _ -> MAP.panic MAP.AArch32Eval "postARMTermStmtAbsState" ["ReturnIf could not interpret next PC: " ++ show (regState ^. MC.curIP)]
-    AA.ReturnIfNot _ ->
-      case simplifyValue (regState ^. MC.curIP) of
-        Just (MC.RelocatableValue _ addr)
-          | Just nextPC <- MM.asSegmentOff mem (MM.incAddr 4 addr) -> do
-              let params = MA.CallParams { MA.postCallStackDelta = 0
-                                         , MA.preserveReg = preservePred
-                                         , MA.stackGrowsDown = True
-                                         }
-              Just (nextPC, MA.absEvalCall params s0 regState nextPC, MJ.postCallBounds params jumpBounds regState)
-        _ -> MAP.panic MAP.AArch32Eval "postARMTermStmtAbsState" ["ReturnIfNot could not interpret next PC: " ++ show (regState ^. MC.curIP)]
 
 preserveRegAcrossSyscall :: MC.ArchReg ARM.AArch32 tp -> Bool
 preserveRegAcrossSyscall r =

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

@@ -10,6 +10,7 @@ module Data.Macaw.ARM.Identify
     , identifyReturn
     , isReturnValue
     , conditionalReturnClassifier
+    , conditionalCallClassifier
     ) where
 
 import           Control.Applicative ( (<|>) )
@@ -29,6 +30,7 @@ import qualified Data.Macaw.Memory as MM
 import qualified Data.Macaw.Memory.Permissions as MMP
 import qualified Data.Macaw.SemMC.Simplify as MSS
 import qualified Data.Macaw.Types as MT
+import           Data.Maybe ( maybeToList )
 import qualified Data.Sequence as Seq
 
 import qualified SemMC.Architecture.AArch32 as ARM
@@ -234,3 +236,116 @@ conditionalReturnClassifier = do
     Jmp.TrueFeasibleBranch _ -> fail "Infeasible false branch"
     Jmp.FalseFeasibleBranch _ -> fail "Infeasible true branch"
     Jmp.InfeasibleBranch -> fail "Branch targets are both infeasible"
+
+data CallsOnBranch = CallsOnTrue | CallsOnFalse
+  deriving (Eq)
+
+-- | Takes a conditionally-set PC and LR value pair and, if they are the same, returns the value
+--
+-- The observation backing this is that there are two cases for a conditional
+-- call. First, assume that the condition evaluates to true (i.e., the call is
+-- issued).  In that case, the fallthrough address (which would have been taken
+-- if the condition was false) and the value in the LR should be the same
+-- (modulo thumb mode switching).
+--
+-- The other case, assuming that the call is not taken, is symmetric.
+--
+-- As a result, the caller ('identifyConditionalCall') is expected to call this
+-- twice, once with @(pc_t, lr_f)@ and again with @(pc_f, lr_t)@.
+--
+-- Note that this classifier helper does not use the abstract transfer function
+-- because return addresses should be literals that don't need any interpretation.
+asConditionalCallReturnAddress
+  :: MC.Memory 32
+  -> MC.Value ARM.AArch32 ids (MT.BVType (MC.ArchAddrWidth ARM.AArch32))
+  -- ^ The value of the PC at one condition polarity
+  -> MC.Value ARM.AArch32 ids (MT.BVType (MC.ArchAddrWidth ARM.AArch32))
+  -- ^ The value of the LR at the other condition polarity
+  -> MAI.Classifier (MC.ArchSegmentOff ARM.AArch32)
+asConditionalCallReturnAddress mem pc_val lr_val = do
+  Just memAddr_pc <- return (MC.valueAsMemAddr pc_val)
+  Just memAddr_lr <- return (MC.valueAsMemAddr lr_val)
+  Just segOff_pc <- return (MC.asSegmentOff mem memAddr_pc)
+  Just segOff_lr <- return (MC.asSegmentOff mem memAddr_lr)
+  when (not (segOff_pc == segOff_lr) || not (isExecutableSegOff segOff_lr)) $ do
+    fail ("Conditional call return address is not executable: " ++ show (memAddr_lr))
+  return segOff_lr
+
+-- | This is a conditional call if the PC and LR are both muxes. Note that we
+-- don't really care what the call target is (and cannot validate it, since it
+-- could be a complex computed value). We primarily care that the conditional LR
+-- value is a valid return address *and* is equal to one of the possible next PC
+-- values.
+--
+-- Note that we return the condition on the PC and not the LR. Ideally they
+-- should be the same, but we aren't currently checking that.
+identifyConditionalCall
+  :: MC.Memory 32
+  -> Seq.Seq (MC.Stmt ARM.AArch32 ids)
+  -> MC.RegState (MC.ArchReg ARM.AArch32) (MC.Value ARM.AArch32 ids)
+  -> MAI.Classifier ( MC.Value ARM.AArch32 ids MT.BoolType    -- Condition
+                    , MC.Value ARM.AArch32 ids (MT.BVType 32) -- Call target
+                    , MC.Value ARM.AArch32 ids (MT.BVType 32) -- Raw link register value
+                    , MC.ArchSegmentOff ARM.AArch32           -- Return address (also the fallthrough address) decoded into a segment offset
+                    , CallsOnBranch                           -- Which branch the call actually occurs on
+                    , Seq.Seq (MC.Stmt ARM.AArch32 ids)       -- The modified statement list
+                    )
+identifyConditionalCall mem stmts s
+  | not (null stmts)
+  , Just (MC.Mux _ pc_c pc_t pc_f) <- simplifiedMux (s ^. MC.boundValue MC.ip_reg)
+  , Just (MC.Mux _ _lr_c lr_t lr_f) <- simplifiedMux (s ^. MC.boundValue AR.arm_LR) =
+      case asConditionalCallReturnAddress mem pc_t lr_f of
+        MAI.ClassifySucceeded _ nextIP ->
+          return (pc_c, pc_f, lr_f, nextIP, CallsOnFalse, stmts)
+        MAI.ClassifyFailed _ -> do
+          nextIP <- asConditionalCallReturnAddress mem pc_f lr_t
+          return (pc_c, pc_t, lr_t, nextIP, CallsOnTrue, stmts)
+  | otherwise = fail "IP is not a mux"
+
+extractCallTargets
+  :: MC.Memory 32
+  -> MC.Value ARM.AArch32 ids (MT.BVType 32)
+  -> [MC.ArchSegmentOff ARM.AArch32]
+extractCallTargets mem val =
+  case val of
+    MC.BVValue _ x -> maybeToList $ MM.resolveAbsoluteAddr mem (fromInteger x)
+    MC.RelocatableValue _ a -> maybeToList $ MM.asSegmentOff mem a
+    MC.SymbolValue {} -> []
+    MC.AssignedValue {} -> []
+    MC.Initial {} -> []
+
+-- | Classify ARM-specific conditional calls
+--
+-- This has the same rationale as 'conditionalReturnClassifier'; core macaw does
+-- not have a representation of conditional calls, so we need to introduce
+-- architecture-specific terminators for them.
+conditionalCallClassifier :: MAI.BlockClassifier ARM.AArch32 ids
+conditionalCallClassifier = do
+  stmts <- CMR.asks MAI.classifierStmts
+  mem <- CMR.asks (MAI.pctxMemory . MAI.classifierParseContext)
+  regs <- CMR.asks MAI.classifierFinalRegState
+  absState <- CMR.asks MAI.classifierAbsState
+  (cond, callTarget, returnAddr, fallthroughIP, callBranch, stmts') <- MAI.liftClassifier (identifyConditionalCall mem stmts regs)
+  let term = if callBranch == CallsOnTrue
+             then Arch.CallIf cond callTarget returnAddr
+             else Arch.CallIfNot cond callTarget returnAddr
+  writtenAddrs <- CMR.asks MAI.classifierWrittenAddrs
+  jmpBounds <- CMR.asks MAI.classifierJumpBounds
+  ainfo <- CMR.asks (MAI.pctxArchInfo . MAI.classifierParseContext)
+
+  case Jmp.postBranchBounds jmpBounds regs cond of
+    Jmp.BothFeasibleBranch trueJumpState falseJumpState -> do
+      let abs' = MDC.branchBlockState ainfo absState stmts regs cond (callBranch == CallsOnFalse)
+      let fallthroughTarget = ( fallthroughIP
+                              , abs'
+                              , if callBranch == CallsOnTrue then falseJumpState else trueJumpState
+                              )
+      return Parsed.ParsedContents { Parsed.parsedNonterm = F.toList stmts'
+                                   , Parsed.parsedTerm = Parsed.ParsedArchTermStmt term regs (Just fallthroughIP)
+                                   , Parsed.intraJumpTargets = [fallthroughTarget]
+                                   , Parsed.newFunctionAddrs = extractCallTargets mem callTarget
+                                   , Parsed.writtenCodeAddrs = writtenAddrs
+                                   }
+    Jmp.TrueFeasibleBranch _ -> fail "Infeasible false branch"
+    Jmp.FalseFeasibleBranch _ -> fail "Infeasible true branch"
+    Jmp.InfeasibleBranch -> fail "Branch targets are both infeasible"

macaw-aarch32/tests/arm/test-conditional-call-a32.mcw.expected

@@ -0,0 +1,5 @@
+R { funcs =  [ (0x100d8, [ (0x100d8, 52)])
+             , (0x1010c, [ (0x1010c, 36), (0x10130, 12)])
+             ]
+  , ignoreBlocks = [0x1013c]
+  }

macaw-aarch32/tests/arm/test-conditional-call.s

@@ -0,0 +1,101 @@
+	.arch armv7-a
+	.eabi_attribute 28, 1
+	.eabi_attribute 20, 1
+	.eabi_attribute 21, 1
+	.eabi_attribute 23, 3
+	.eabi_attribute 24, 1
+	.eabi_attribute 25, 1
+	.eabi_attribute 26, 2
+	.eabi_attribute 30, 6
+	.eabi_attribute 34, 1
+	.eabi_attribute 18, 4
+	.file	"test-direct-call.c"
+	.text
+	.global	g
+	.bss
+	.align	2
+	.type	g, %object
+	.size	g, 4
+g:
+	.space	4
+	.text
+	.align	2
+	.global	f2
+	.arch armv7-a
+	.syntax unified
+	.arm
+	.fpu vfpv3-d16
+	.type	f2, %function
+f2:
+	@ args = 0, pretend = 0, frame = 8
+	@ frame_needed = 1, uses_anonymous_args = 0
+	@ link register save eliminated.
+	str	fp, [sp, #-4]!
+	add	fp, sp, #0
+	sub	sp, sp, #12
+	str	r0, [fp, #-8]
+	ldr	r3, [fp, #-8]
+	add	r2, r3, #2
+	movw	r3, #:lower16:g
+	movt	r3, #:upper16:g
+	str	r2, [r3]
+	nop
+	add	sp, fp, #0
+	@ sp needed
+	ldr	fp, [sp], #4
+	bx	lr
+	.size	f2, .-f2
+	.align	2
+	.global	f1
+	.syntax unified
+	.arm
+	.fpu vfpv3-d16
+	.type	f1, %function
+f1:
+	@ args = 0, pretend = 0, frame = 8
+	@ frame_needed = 1, uses_anonymous_args = 0
+	push	{fp, lr}
+	add	fp, sp, #4
+	sub	sp, sp, #8
+	str	r0, [fp, #-8]
+	ldr	r3, [fp, #-8]
+	add	r3, r3, #1
+	mov	r0, r3
+  cmp r0, #0
+	blne	f2
+	nop
+	sub	sp, fp, #4
+	@ sp needed
+	pop	{fp, pc}
+	.size	f1, .-f1
+	.align	2
+	.global	_start
+	.syntax unified
+	.arm
+	.fpu vfpv3-d16
+	.type	_start, %function
+_start:
+	@ args = 0, pretend = 0, frame = 0
+	@ frame_needed = 1, uses_anonymous_args = 0
+	push	{fp, lr}
+	add	fp, sp, #4
+	movw	r3, #:lower16:g
+	movt	r3, #:upper16:g
+	mov	r2, #0
+	str	r2, [r3]
+	mov	r0, #5
+	bl	f1
+	.syntax divided
+@ 16 "test-direct-call.c" 1
+	mov     %r7, $1
+@ 0 "" 2
+@ 16 "test-direct-call.c" 1
+	svc #0
+@ 0 "" 2
+	.arm
+	.syntax unified
+	nop
+	pop	{fp, pc}
+	.size	_start, .-_start
+	.ident	"GCC: (GNU) 11.2.1 20210728 (Red Hat Cross 11.2.1-1)"
+	.section	.note.GNU-stack,"",%progbits

symbolic/src/Data/Macaw/Symbolic/Backend.hs

@@ -11,6 +11,9 @@ module Data.Macaw.Symbolic.Backend (
     -- $archBackend
     CG.MacawArchStmtExtension
   , CG.CrucGen
+  , CG.translateFns
+  , CG.crucRegisterReg
+  , CG.mkAtom
   , PS.macawAssignToCrucM
   , CG.valueToCrucible
   , CG.evalArchStmt

symbolic/src/Data/Macaw/Symbolic/CrucGen.hs

@@ -43,12 +43,15 @@ module Data.Macaw.Symbolic.CrucGen
   , MacawArchStmtExtension
     -- ** Operations for implementing new backends.
   , CrucGen
+  , translateFns
+  , crucRegisterReg
   , MacawMonad
   , runMacawMonad
   , addMacawBlock
   , mmFreshNonce
   , mmNonceGenerator
   , mmExecST
+  , mkAtom
   , BlockLabelMap
   , addParsedBlock
   , valueToCrucible