Add support for more instructions

semmc has semantics for many new instructions.  We also added support for
translating the count leading zero functions.

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

submodules/semmc

@@ -1 +1 @@
-Subproject commit ec5030f68aad2ace63916f1093a8cf36a466afd6
+Subproject commit 7518554cf212b28d5689ebf661af027fb8ef0e09