Improve alloc_aligned commands. (#648)

Add `crucible_alloc_readonly_aligned` command. Allow
`crucible_alloc_aligned`/`crucible_alloc_readonly_aligned` to specify an
alignment less than the default alignment of the type.

Co-authored-by: brianhuffman <[email protected]>

Author: andreistefanescu

Diff for: src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -46,6 +46,7 @@ module SAWScript.Crucible.LLVM.Builtins
     , crucible_alloc
     , crucible_alloc_aligned
     , crucible_alloc_readonly
+    , crucible_alloc_readonly_aligned
     , crucible_alloc_with_size
     , crucible_alloc_global
     , crucible_fresh_expanded_val
@@ -1485,10 +1486,10 @@ crucible_alloc_with_mutability_and_size mut sz alignment bic opts lty =
      alignment' <-
        case alignment of
          Just a -> do
-           when (a < memTyAlign) $ fail $ unlines
-             [ "User error: manually-specified alignment was less than needed"
+           when (a < memTyAlign) $ liftIO $ printOutLn opts Info $ unlines
+             [ "Warning: manually-specified alignment was less than default for type"
              , "Allocation type: " ++ show memTy
-             , "Minimum alignment for type: " ++ show (Crucible.fromAlignment memTyAlign) ++ "-byte"
+             , "Default alignment for type: " ++ show (Crucible.fromAlignment memTyAlign) ++ "-byte"
              , "Specified alignment: " ++ show (Crucible.fromAlignment a) ++ "-byte"
              ]
            pure a
@@ -1517,28 +1518,50 @@ crucible_alloc_aligned ::
   Int            ->
   L.Type         ->
   LLVMCrucibleSetupM (AllLLVM SetupValue)
-crucible_alloc_aligned bic opts n lty =
+crucible_alloc_aligned =
+  crucible_alloc_aligned_with_mutability Crucible.Mutable
+
+crucible_alloc_readonly ::
+  BuiltinContext ->
+  Options        ->
+  L.Type         ->
+  LLVMCrucibleSetupM (AllLLVM SetupValue)
+crucible_alloc_readonly =
+  crucible_alloc_with_mutability_and_size Crucible.Immutable Nothing Nothing
+
+crucible_alloc_readonly_aligned ::
+  BuiltinContext ->
+  Options        ->
+  Int            ->
+  L.Type         ->
+  LLVMCrucibleSetupM (AllLLVM SetupValue)
+crucible_alloc_readonly_aligned =
+  crucible_alloc_aligned_with_mutability Crucible.Immutable
+
+crucible_alloc_aligned_with_mutability ::
+  Crucible.Mutability ->
+  BuiltinContext ->
+  Options ->
+  Int ->
+  L.Type ->
+  LLVMCrucibleSetupM (AllLLVM SetupValue)
+crucible_alloc_aligned_with_mutability mut bic opts n lty =
   case Crucible.toAlignment (Crucible.toBytes n) of
     Nothing ->
-      LLVMCrucibleSetupM $ fail $
-      "crucible_alloc_aligned: invalid non-power-of-2 alignment: " ++ show n
+      LLVMCrucibleSetupM $ fail $ unwords
+        [ "crucible_alloc_aligned/crucible_alloc_readonly_aligned:"
+        , "invalid non-power-of-2 alignment:"
+        , show n
+        ]
     Just alignment ->
       crucible_alloc_with_mutability_and_size
-        Crucible.Mutable
+        mut
         Nothing
         (Just alignment)
         bic
         opts
         lty
 
-crucible_alloc_readonly ::
-  BuiltinContext ->
-  Options        ->
-  L.Type         ->
-  LLVMCrucibleSetupM (AllLLVM SetupValue)
-crucible_alloc_readonly =
-  crucible_alloc_with_mutability_and_size Crucible.Immutable Nothing Nothing
-
 crucible_alloc_with_size ::
   BuiltinContext ->
   Options        ->

Diff for: src/SAWScript/Interpreter.hs

@@ -1816,8 +1816,7 @@ primitives = Map.fromList
     [ "Declare that a memory region of the given type should be allocated in"
     , "a Crucible specification, and also specify that the start of the region"
     , "should be aligned to a multiple of the specified number of bytes (which"
-    , "must be a power of 2). The specified alignment must be no less than the"
-    , "minimum required by the LLVM type."
+    , "must be a power of 2)."
     ]
 
   , prim "crucible_alloc_readonly" "LLVMType -> CrucibleSetup SetupValue"
@@ -1830,6 +1829,18 @@ primitives = Map.fromList
     , "read-only regions."
     ]
 
+  , prim "crucible_alloc_readonly_aligned" "Int -> LLVMType -> CrucibleSetup SetupValue"
+    (bicVal crucible_alloc_readonly_aligned)
+    Current
+    [ "Declare that a read-only memory region of the given type should be"
+    , "a Crucible specification, and also specify that the start of the region"
+    , "should be aligned to a multiple of the specified number of bytes (which"
+    , "must be a power of 2). The function must not attempt to write to this"
+    , "memory region. Unlike `crucible_alloc`/`crucible_alloc_aligned`,"
+    , "regions allocated with `crucible_alloc_readonly_aligned` are allowed to"
+    , "alias other read-only regions."
+    ]
+
   , prim "crucible_alloc_with_size" "Int -> LLVMType -> CrucibleSetup SetupValue"
     (bicVal crucible_alloc_with_size)
     Experimental