Support LLVM 15 and 16, opaque pointers

This patch adds support for LLVM 15 and 16 by adding support for opaque
pointers, which are described in https://llvm.org/docs/OpaquePointers.html.  I
have also added a test case involving LLVM bitcode using opaque pointers to
kick the tires and ensure that the basics work as expected.

For the most part, this is a straightforward process, as most uses of pointer
types in SAW already do not care about pointee types. There are some
exceptions, however:

* The `typeOfSetupValue` function, as well as several places that use this
  function, scrutinize pointee types of pointers, which would appear to fly in
  the face of opaque pointers. I attempt to explain in #1876 which this is
  actually OK for now (although a bit awkward).
* The `llvm_boilerplate`/skeleton machinery does not support opaque pointers
  at all. See #1877.

This patch also bumps the following submodules to bring in support for opaque
pointers:

* `llvm-pretty`: GaloisInc/llvm-pretty#110
* `llvm-pretty-bc-parser`: GaloisInc/llvm-pretty-bc-parser#221
* `crucible`: GaloisInc/crucible#1085

This also bumps the `what4` submodule to bring in the changes from
GaloisInc/what4#234. This isn't necessary to support opaque pointers, but it
_is_ necessary to support a build plan involving `tasty-sugar-2.2.*`, which
`llvm-pretty-bc-parser`'s test suite now requires.

CHANGES.md

@@ -99,7 +99,7 @@
   see the `mir_*` commands documented in the
   [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md).
 
-* Support LLVM versions up to 14.
+* Support LLVM versions up to 16.
 
 # Version 0.9
 

README.md

@@ -72,7 +72,7 @@ SAW can analyze LLVM programs (usually derived from C, but potentially
 for other languages). The only tool strictly required for this is a
 compiler that can generate LLVM bitcode, such as `clang`. However,
 having the full LLVM tool suite available can be useful. We have tested
-SAW with LLVM and `clang` versions from 3.5 to 14.0, as well as the
+SAW with LLVM and `clang` versions from 3.5 to 16.0, as well as the
 version of `clang` bundled with Apple Xcode. We welcome bug reports on
 any failure to parse bitcode from LLVM versions in that range.
 

doc/manual/manual.md

@@ -1580,7 +1580,7 @@ The resulting `LLVMModule` can be passed into the various functions
 described below to perform analysis of specific LLVM functions.
 
 The LLVM bitcode parser should generally work with LLVM versions between
-3.5 and 14.0, though it may be incomplete for some versions. Debug
+3.5 and 16.0, though it may be incomplete for some versions. Debug
 metadata has changed somewhat throughout that version range, so is the
 most likely case of incompleteness. We aim to support every version
 after 3.5, however, so report any parsing failures as [on

heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs

@@ -182,9 +182,10 @@ translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr) ixs) =
   translateLLVMValue w tp ptr >>= \ptr_trans ->
   translateLLVMGEP w tp ptr_trans ixs
 translateLLVMConstExpr w (L.ConstConv L.BitCast
-                          (L.Typed tp@(L.PtrTo _) v) (L.PtrTo _)) =
-  -- A bitcast from one LLVM pointer type to another is a no-op for us
-  translateLLVMValue w tp v
+                          (L.Typed fromTp v) toTp)
+  | L.isPointer fromTp && L.isPointer toTp
+  = -- A bitcast from one LLVM pointer type to another is a no-op for us
+    translateLLVMValue w fromTp v
 translateLLVMConstExpr _ ce =
   traceAndZeroM ("translateLLVMConstExpr does not yet handle:\n"
                  ++ ppLLVMConstExpr ce)

intTests/test1132-opaque/Makefile

@@ -0,0 +1,13 @@
+# NB: Ensure that clang-15 or later is used so that the resulting LLVM bitcode
+# uses opaque pointers.
+CC = clang
+CFLAGS = -g -emit-llvm -frecord-command-line -O0
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc

intTests/test1132-opaque/test.c

@@ -0,0 +1,7 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+void f(uint8_t **x) {
+  *x = malloc(sizeof(uint8_t));
+  **x = 42;
+}

intTests/test1132-opaque/test.saw

@@ -0,0 +1,11 @@
+bc <- llvm_load_module "test.bc";
+
+let f_contract = do {
+  x <- llvm_alloc (llvm_pointer (llvm_int 8));
+  llvm_execute_func [x];
+  p <- llvm_alloc (llvm_int 8);
+  llvm_points_to x p;
+  llvm_points_to p (llvm_term {{ 42 : [8] }});
+};
+
+llvm_verify bc "f" [] false f_contract abc;

intTests/test1132-opaque/test.sh

@@ -0,0 +1,5 @@
+# A variant of test1132 that instead uses opaque pointers to ensure that the
+# basics of SAW work in an opaque pointer context.
+set -e
+
+$SAW test.saw

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -2124,15 +2124,24 @@ cryptolTypeOfActual dl mt =
       do cty <- cryptolTypeOfActual dl ty
          return $ Cryptol.tSeq (Cryptol.tNum n) cty
     Crucible.PtrType _ ->
-      return $ Cryptol.tWord (Cryptol.tNum (Crucible.ptrBitwidth dl))
+      return cryptolPtrType
+    Crucible.PtrOpaqueType ->
+      return cryptolPtrType
     Crucible.StructType si ->
       do let memtypes = V.toList (Crucible.siFieldTypes si)
          ctys <- traverse (cryptolTypeOfActual dl) memtypes
          case ctys of
            [cty] -> return cty
            _ -> return $ Cryptol.tTuple ctys
-    _ ->
+    Crucible.X86_FP80Type ->
       Nothing
+    Crucible.VecType{} ->
+      Nothing
+    Crucible.MetadataType ->
+      Nothing
+  where
+    cryptolPtrType :: Cryptol.Type
+    cryptolPtrType = Cryptol.tWord (Cryptol.tNum (Crucible.ptrBitwidth dl))
 
 -- | Generate a fresh variable term. The name will be used when
 -- pretty-printing the variable in debug output.
@@ -2227,6 +2236,13 @@ constructExpandedSetupValue cc sc loc t =
     Crucible.MetadataType   -> failUnsupportedType "Metadata"
     Crucible.VecType{}      -> failUnsupportedType "Vec"
     Crucible.X86_FP80Type{} -> failUnsupportedType "X86_FP80"
+    -- This case is a bit suspect, but it _should_ be unreachable under the
+    -- assumption that a SAW LLVMType value cannot represent an opaque pointer.
+    -- I (RGS) believe this to be the case, as the only way to construct a
+    -- pointer LLVMType at the moment is to use `llvm_pointer`, which constructs
+    -- a non-opaque pointer type. If we ever added something like, say,
+    -- `llvm_pointer_opaque`, we would need to reconsider this case.
+    Crucible.PtrOpaqueType  -> failUnsupportedType "PtrOpaque"
   where failUnsupportedType tyName = throwCrucibleSetup loc $ unwords
           ["llvm_fresh_expanded_var: " ++ tyName ++ " not supported"]
 

src/SAWScript/Crucible/LLVM/Override.hs

@@ -1241,9 +1241,15 @@ diffMemTypes x0 y0 =
     (Crucible.IntType x, Crucible.IntType y) | x == y -> []
     (Crucible.FloatType, Crucible.FloatType) -> []
     (Crucible.DoubleType, Crucible.DoubleType) -> []
-    (Crucible.PtrType{}, Crucible.PtrType{}) -> []
-    (Crucible.IntType w, Crucible.PtrType{}) | w == wptr -> []
-    (Crucible.PtrType{}, Crucible.IntType w) | w == wptr -> []
+    (_, _)
+      | Crucible.isPointerMemType x0 && Crucible.isPointerMemType y0 ->
+          []
+    (Crucible.IntType w, _)
+      | Crucible.isPointerMemType y0 && w == wptr ->
+          []
+    (_, Crucible.IntType w)
+      | Crucible.isPointerMemType x0 && w == wptr ->
+          []
     (Crucible.ArrayType xn xt, Crucible.ArrayType yn yt)
       | xn == yn ->
         [ (Nothing : path, l , r) | (path, l, r) <- diffMemTypes xt yt ]
@@ -1314,15 +1320,15 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
                               (V.toList (Crucible.fiType <$> Crucible.siFields fields))
                               zs ]
 
-    (Crucible.LLVMValInt blk off, Crucible.PtrType _, SetupElem () v i) ->
+    (Crucible.LLVMValInt blk off, _, SetupElem () v i) | Crucible.isPointerMemType expectedTy ->
       do let tyenv = MS.csAllocations cs
              nameEnv = MS.csTypeNames cs
          delta <- exceptToFail $ resolveSetupElemOffset cc tyenv nameEnv v i
          off' <- liftIO $ W4.bvSub sym off
            =<< W4.bvLit sym (W4.bvWidth off) (Crucible.bytesToBV (W4.bvWidth off) delta)
          matchArg opts sc cc cs prepost md (Crucible.LLVMValInt blk off') expectedTy v
 
-    (Crucible.LLVMValInt blk off, Crucible.PtrType _, SetupField () v n) ->
+    (Crucible.LLVMValInt blk off, _, SetupField () v n) | Crucible.isPointerMemType expectedTy ->
       do let tyenv = MS.csAllocations cs
              nameEnv = MS.csTypeNames cs
          fld <- exceptToFail $

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -473,8 +473,8 @@ typeOfSetupValue cc env nameEnv val =
 
     SetupCast () v ltp ->
       do memTy <- typeOfSetupValue cc env nameEnv v
-         case memTy of
-           Crucible.PtrType _symTy ->
+         if Crucible.isPointerMemType memTy
+           then
              case let ?lc = lc in Crucible.liftMemType (L.PtrTo ltp) of
                Left err -> throwError $ unlines
                              [ "typeOfSetupValue: invalid type " ++ show ltp
@@ -483,10 +483,11 @@ typeOfSetupValue cc env nameEnv val =
                              ]
                Right mt -> pure mt
 
-           _ -> throwError $ unwords $
-                  [ "typeOfSetupValue: tried to cast the type of a non-pointer value"
-                  , "actual type of value: " ++ show memTy
-                  ]
+           else
+             throwError $ unwords $
+               [ "typeOfSetupValue: tried to cast the type of a non-pointer value"
+               , "actual type of value: " ++ show memTy
+               ]
 
     SetupElem () v i -> do
       do memTy <- typeOfSetupValue cc env nameEnv v

src/SAWScript/Crucible/LLVM/X86.hs

@@ -1158,7 +1158,7 @@ setArgs env tyenv nameEnv args
       let
         setRegSetupValue rs (reg, sval) =
           exceptToFail (typeOfSetupValue cc tyenv nameEnv sval) >>= \case
-            C.LLVM.PtrType _ -> do
+            ty | C.LLVM.isPointerMemType ty -> do
               val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64)
                 =<< resolveSetupVal cc mem env tyenv nameEnv sval
               setReg reg val rs