cmpxchg: Compare argument types using eqTypeModuloOpaquePtrs

Because `llvm-pretty` permits opaque and non-opaque pointers to coexist, it is possible for the first argument of `cmpxchg` to be an opaque pointer and the second argument to be a non-opaque pointer (or vice versa). We don't want to reject such scenarios, so we compare the types of the argument using `eqTypeModuloOpaquePtrs`, a special form of type equality that treats opaque and non-opaque pointers as being the same. See #177. This requires bumping the `llvm-pretty` submodule to bring in the corresponding changes from GaloisInc/llvm-pretty#110.
GaloisInc · May 30, 2023 · 2e848a6 · 2e848a6
1 parent 0313fe9
commit 2e848a6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/llvm-pretty b/llvm-pretty
diff --git a/src/Data/LLVM/BitCode/IR/Function.hs b/src/Data/LLVM/BitCode/IR/Function.hs
@@ -868,7 +868,7 @@ parseFunctionBlockEntry _ t d (fromEntry -> Just r) = case recordCode r of
     -- TODO: record size assertion
     -- Assert.recordSizeGreater r (ix'' + 5)
 
-    when (typedType val /= typedType new) $ fail $ unlines $
+    when (typedType val `eqTypeModuloOpaquePtrs` typedType new) $ fail $ unlines $
       [ "Mismatched value types:"
       , "cmp value: " ++ show (typedValue val)
       , "new value: " ++ show (typedValue new)