diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs index fabe3a9b..97ed98b2 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -447,6 +447,24 @@ evalNonceAppTH bvi nonceApp = addExpr (AppExpr (M.BVTestBit bitNumExp locExp)) |] _ -> fail ("Unsupported argument list for test_bit_dynamic: " ++ showF args) + -- For count leading zeros, we don't have a SimpleBuilder term to reduce + -- it to, so we have to manually transform it to macaw here (i.e., we + -- can't use the more general substitution method, since that is in + -- terms of rewriting simplebuilder). + "clz_32" -> + case FC.toListFC Some args of + [Some loc] -> do + [| do locExp <- $(addEltTH bvi loc) + addExpr (AppExpr (M.Bsr (NR.knownNat @32) locExp)) + |] + _ -> fail ("Unsupported argument list for clz: " ++ showF args) + "clz_64" -> + case FC.toListFC Some args of + [Some loc] -> do + [| do locExp <- $(addEltTH bvi loc) + addExpr (AppExpr (M.Bsr (NR.knownNat @64) locExp)) + |] + _ -> fail ("Unsupported argument list for clz: " ++ showF args) _ | Just nBytes <- readMemBytes fnName -> do case FC.toListFC Some args of [_, Some addrElt] -> do diff --git a/submodules/semmc b/submodules/semmc index ec5030f6..7518554c 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit ec5030f68aad2ace63916f1093a8cf36a466afd6 +Subproject commit 7518554cf212b28d5689ebf661af027fb8ef0e09