[ppc] Fix an issue with floating point translation

The change is actually in the semantics (semmc), where we were extracting the
wrong part of the 128 bit vector registers to operate on.  Many operations were
being simplified to zero, which manifest as unused fprc registers.

macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs

@@ -514,7 +514,7 @@ floatingPointTH bvi fnName args =
           [| do fpval <- $(addEltTH bvi a)
                 addExpr (AppExpr (M.FPAbs M.DoubleFloatRepr fpval))
            |]
-        "negate64" ->
+        "negate64" -> do
           [| do fpval <- $(addEltTH bvi a)
                 addExpr (AppExpr (M.FPNeg M.DoubleFloatRepr fpval))
            |]
@@ -568,7 +568,7 @@ floatingPointTH bvi fnName args =
         _ -> fail ("Unsupported binary floating point intrinsic: " ++ fnName)
     [Some a, Some b, Some c] ->
       case fnName of
-        "muladd64" ->
+        "muladd64" -> do
           -- FIXME: This is very wrong - we need a separate constructor for it
           -- a * c + b
           [| do valA <- $(addEltTH bvi a)
@@ -788,14 +788,13 @@ crucAppToExprTH elt interps = case elt of
      |]
   _ -> [| error "unsupported Crucible elt" |]
 
-
-
 locToRegTH :: (1 <= APPC.ArchRegWidth ppc,
                M.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc)
            => proxy ppc
            -> APPC.Location ppc ctp
            -> Q Exp
 locToRegTH _ (APPC.LocGPR (D.GPR gpr)) = [| PPC_GP (D.GPR $(lift gpr)) |]
+locToRegTH _ (APPC.LocVSR (D.VSReg vsr)) = [| PPC_FR (D.VSReg $(lift vsr)) |]
 locToRegTH _  APPC.LocIP       = [| PPC_IP |]
 locToRegTH _  APPC.LocLNK      = [| PPC_LNK |]
 locToRegTH _  APPC.LocCTR      = [| PPC_CTR |]

submodules/semmc

@@ -1 +1 @@
-Subproject commit 8848a5d1ca0e5bc6d4ca924fcaeb9c40df76c142
+Subproject commit a8ede2ccbc0e72f2086b1156dc6dca2a687c0ace