Skip to content

Commit 89ae791

Browse files
RyanGlScottRyanGlScott
committed
Broaden scope of read-unwritten-memory to lax-loads-and-stores
This renamed the `read-unwritten-memory` Crux option to `lax-loads-and-stores`, reflecting its new purpose of being a catch-all option for relaxing various validity checks related to loads and stores. This is meant for SV-COMP mode, which has a different view of fatal errors than Crucible does. This addresses some of the goals of #783. It does not address the goal of designing a generic taxonomy of errors.
1 parent 9be976e commit 89ae791

File tree

15 files changed

+103
-31
lines changed

15 files changed

+103
-31
lines changed

‎crucible-llvm/crucible-llvm.cabal

+1
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,7 @@ library
108108
Lang.Crucible.LLVM.Translation.Options
109109
Lang.Crucible.LLVM.Translation.Types
110110
Lang.Crucible.LLVM.Types
111+
Lang.Crucible.LLVM.Utils
111112

112113
if impl(ghc >= 8.6)
113114
default-extensions: NoStarIsType

‎crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs

+17-8
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
{-# LANGUAGE FlexibleContexts #-}
1414
{-# LANGUAGE FlexibleInstances #-}
1515
{-# LANGUAGE GADTs #-}
16+
{-# LANGUAGE ImplicitParams #-}
1617
{-# LANGUAGE ImpredicativeTypes #-}
1718
{-# LANGUAGE MultiParamTypeClasses #-}
1819
{-# LANGUAGE OverloadedStrings #-}
@@ -180,7 +181,8 @@ llvmStackrestore =
180181
(\_memOps _sym _args -> return ())
181182

182183
llvmMemmoveOverride_8_8_32
183-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
184+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
185+
, ?memOpts :: MemOptions )
184186
=> LLVMOverride p sym
185187
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr
186188
::> BVType 32 ::> BVType 32 ::> BVType 1)
@@ -190,7 +192,8 @@ llvmMemmoveOverride_8_8_32 =
190192
(\memOps sym args -> Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemmove sym memOps dst src len v) args)
191193

192194
llvmMemmoveOverride_8_8_32_noalign
193-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
195+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
196+
, ?memOpts :: MemOptions )
194197
=> LLVMOverride p sym
195198
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr
196199
::> BVType 32 ::> BVType 1)
@@ -201,7 +204,8 @@ llvmMemmoveOverride_8_8_32_noalign =
201204

202205

203206
llvmMemmoveOverride_8_8_64
204-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
207+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
208+
, ?memOpts :: MemOptions )
205209
=> LLVMOverride p sym
206210
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr
207211
::> BVType 64 ::> BVType 32 ::> BVType 1)
@@ -212,7 +216,8 @@ llvmMemmoveOverride_8_8_64 =
212216

213217

214218
llvmMemmoveOverride_8_8_64_noalign
215-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
219+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
220+
, ?memOpts :: MemOptions )
216221
=> LLVMOverride p sym
217222
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr
218223
::> BVType 64 ::> BVType 1)
@@ -274,7 +279,8 @@ llvmMemsetOverride_8_32_noalign =
274279

275280

276281
llvmMemcpyOverride_8_8_32
277-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
282+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
283+
, ?memOpts :: MemOptions )
278284
=> LLVMOverride p sym
279285
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr
280286
::> BVType 32 ::> BVType 32 ::> BVType 1)
@@ -284,7 +290,8 @@ llvmMemcpyOverride_8_8_32 =
284290
(\memOps sym args -> Ctx.uncurryAssignment (\dst src len _align v -> Libc.callMemcpy sym memOps dst src len v) args)
285291

286292
llvmMemcpyOverride_8_8_32_noalign
287-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
293+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
294+
, ?memOpts :: MemOptions )
288295
=> LLVMOverride p sym
289296
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr
290297
::> BVType 32 ::> BVType 1)
@@ -295,7 +302,8 @@ llvmMemcpyOverride_8_8_32_noalign =
295302

296303

297304
llvmMemcpyOverride_8_8_64
298-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
305+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
306+
, ?memOpts :: MemOptions )
299307
=> LLVMOverride p sym
300308
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr
301309
::> BVType 64 ::> BVType 32 ::> BVType 1)
@@ -306,7 +314,8 @@ llvmMemcpyOverride_8_8_64 =
306314

307315

308316
llvmMemcpyOverride_8_8_64_noalign
309-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
317+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
318+
, ?memOpts :: MemOptions )
310319
=> LLVMOverride p sym
311320
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr
312321
::> BVType 64 ::> BVType 1)

‎crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs

+10-5
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,8 @@ import Lang.Crucible.LLVM.Intrinsics.Options
6767

6868

6969
llvmMemcpyOverride
70-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
70+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
71+
, ?memOpts :: MemOptions )
7172
=> LLVMOverride p sym
7273
(EmptyCtx ::> LLVMPointerType wptr
7374
::> LLVMPointerType wptr
@@ -84,7 +85,8 @@ llvmMemcpyOverride =
8485

8586

8687
llvmMemcpyChkOverride
87-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
88+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
89+
, ?memOpts :: MemOptions )
8890
=> LLVMOverride p sym
8991
(EmptyCtx ::> LLVMPointerType wptr
9092
::> LLVMPointerType wptr
@@ -102,7 +104,8 @@ llvmMemcpyChkOverride =
102104
)
103105

104106
llvmMemmoveOverride
105-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
107+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
108+
, ?memOpts :: MemOptions )
106109
=> LLVMOverride p sym
107110
(EmptyCtx ::> (LLVMPointerType wptr)
108111
::> (LLVMPointerType wptr)
@@ -378,7 +381,8 @@ callFree sym mvar
378381
-- *** Memory manipulation
379382

380383
callMemcpy
381-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
384+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
385+
, ?memOpts :: MemOptions )
382386
=> sym
383387
-> GlobalVar Mem
384388
-> RegEntry sym (LLVMPointerType wptr)
@@ -400,7 +404,8 @@ callMemcpy sym mvar
400404
-- ranges are disjoint. The underlying operation
401405
-- works correctly in both cases.
402406
callMemmove
403-
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
407+
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
408+
, ?memOpts :: MemOptions )
404409
=> sym
405410
-> GlobalVar Mem
406411
-> RegEntry sym (LLVMPointerType wptr)

‎crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

+5-2
Original file line numberDiff line numberDiff line change
@@ -243,6 +243,7 @@ import Lang.Crucible.LLVM.MemModel.Options
243243
import Lang.Crucible.LLVM.MemModel.Value
244244
import Lang.Crucible.LLVM.Translation.Constant
245245
import Lang.Crucible.LLVM.Types
246+
import Lang.Crucible.LLVM.Utils
246247
import Lang.Crucible.Panic (panic)
247248

248249

@@ -912,7 +913,8 @@ doArrayConstStore sym mem ptr alignment arr len = do
912913
-- Precondition: the source and destination pointers fall within valid allocated
913914
-- regions.
914915
doMemcpy ::
915-
(1 <= w, IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym) =>
916+
( 1 <= w, IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym
917+
, ?memOpts :: MemOptions ) =>
916918
sym ->
917919
NatRepr w ->
918920
MemImpl sym ->
@@ -931,7 +933,8 @@ doMemcpy sym w mem mustBeDisjoint dest src len = do
931933

932934
let mop = MemCopyOp (gsym_dest, dest) (gsym_src, src) len (memImplHeap mem)
933935

934-
p1' <- Partial.annotateME sym mop UnreadableRegion p1
936+
p1' <- applyUnless (laxLoadsAndStores ?memOpts)
937+
(Partial.annotateME sym mop UnreadableRegion) p1
935938
p2' <- Partial.annotateME sym mop UnwritableRegion p2
936939

937940
assert sym p1' $ AssertFailureSimError "Mem copy failed" "Invalid copy source"

‎crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

+8-3
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,7 @@ import Lang.Crucible.LLVM.MemModel.Type
111111
import Lang.Crucible.LLVM.MemModel.Value
112112
import Lang.Crucible.LLVM.MemModel.Partial (PartLLVMVal, HasLLVMAnn)
113113
import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial
114+
import Lang.Crucible.LLVM.Utils
114115
import Lang.Crucible.Simulator.RegMap (RegValue'(..))
115116

116117
--------------------------------------------------------------------------------
@@ -718,8 +719,12 @@ readMem sym w gsym l tp alignment m = do
718719
-- Otherwise, fall back to the less-optimized read case
719720
_ -> readMem' sym w (memEndianForm m) gsym l m tp alignment (memWrites m)
720721

721-
Partial.attachMemoryError sym p1 mop UnreadableRegion =<<
722-
Partial.attachSideCondition sym p2 (UB.ReadBadAlignment (RV l) alignment) part_val
722+
part_val' <- applyUnless (laxLoadsAndStores ?memOpts)
723+
(Partial.attachSideCondition sym p2 (UB.ReadBadAlignment (RV l) alignment))
724+
part_val
725+
applyUnless (laxLoadsAndStores ?memOpts)
726+
(Partial.attachMemoryError sym p1 mop UnreadableRegion)
727+
part_val'
723728

724729
data CacheEntry sym w =
725730
CacheEntry !(StorageType) !(SymNat sym) !(SymBV sym w)
@@ -767,7 +772,7 @@ readMem' sym w end gsym l0 origMem tp0 alignment (MemWrites ws) =
767772
ReadMem sym (PartLLVMVal sym)
768773
fallback0 tp l =
769774
liftIO $
770-
if readUnwrittenMemory ?memOpts
775+
if laxLoadsAndStores ?memOpts
771776
then Partial.totalLLVMVal sym <$> freshLLVMVal sym tp
772777
else do -- We're playing a trick here. By making a fresh constant a proof obligation, we can be
773778
-- sure it always fails. But, because it's a variable, it won't be constant-folded away

‎crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs

+27-9
Original file line numberDiff line numberDiff line change
@@ -34,29 +34,47 @@ data MemOptions
3434
-- will sometimes compare equal if the compiler decides to
3535
-- consolidate their storage.
3636

37-
, readUnwrittenMemory :: !Bool
38-
-- ^ Should we allow reading from previously unwritten memory? Such a
39-
--- read will return an arbitrary, fixed value of the appropriate type.
37+
, laxLoadsAndStores :: !Bool
38+
-- ^ Should we relax some of Crucible's validity checks for memory loads
39+
-- and stores? If 'True', the following checks will be relaxed:
40+
--
41+
-- * If reading from previously unwritten memory, rather than throw a
42+
-- 'NoSatisfyingWrite' error, the read will return an arbitrary,
43+
-- fixed value of the appropriate type.
44+
--
45+
-- * If reading from a region that isn't allocated or isn't large
46+
-- enough, Crucible will proceed rather than throw an
47+
-- 'UnreadableRegion' error.
48+
--
49+
-- * Reading a value from a pointer with insufficent alignment is not
50+
-- treated as undefined behavior. That is, Crucible will not throw a
51+
-- 'ReadBadAlignment' error.
52+
--
53+
-- This option is primarily useful for SV-COMP, which does not treat
54+
-- the scenarios listed above as fatal errors.
4055
}
4156

4257

43-
-- | The default memory model options require strict adherence to
44-
-- the language standard regarding pointer equality and ordering.
58+
-- | The default memory model options:
59+
--
60+
-- * Require strict adherence to the language standard regarding pointer
61+
-- equality and ordering.
62+
--
63+
-- * Perform Crucible's default validity checks for memory loads and stores.
4564
defaultMemOptions :: MemOptions
4665
defaultMemOptions =
4766
MemOptions
4867
{ laxPointerOrdering = False
4968
, laxConstantEquality = False
50-
, readUnwrittenMemory = False
69+
, laxLoadsAndStores = False
5170
}
5271

5372

54-
-- | The lax pointer memory options allow pointer ordering comparisons
73+
-- | Like 'defaultMemOptions', but allow pointer ordering comparisons
5574
-- and equality comparisons of pointers to constant data.
5675
laxPointerMemOptions :: MemOptions
5776
laxPointerMemOptions =
58-
MemOptions
77+
defaultMemOptions
5978
{ laxPointerOrdering = True
6079
, laxConstantEquality = True
61-
, readUnwrittenMemory = False
6280
}

‎crucible-llvm/src/Lang/Crucible/LLVM/Utils.hs

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
------------------------------------------------------------------------
2+
-- |
3+
-- Module : Lang.Crucible.LLVM.Utils
4+
-- Description : Miscellaneous utility functions.
5+
-- Copyright : (c) Galois, Inc 2021
6+
-- License : BSD3
7+
-- Maintainer : Rob Dockins <[email protected]>
8+
-- Stability : provisional
9+
------------------------------------------------------------------------
10+
module Lang.Crucible.LLVM.Utils (applyUnless) where
11+
12+
-- | If the first argument is 'False', apply the second argument to the third.
13+
-- Otherwise, simply return the third argument.
14+
applyUnless :: Applicative f => Bool -> (a -> f a) -> a -> f a
15+
applyUnless b f x = if b then pure x else f x

‎crux-llvm/src/Crux/LLVM/Config.hs

+3-3
Original file line numberDiff line numberDiff line change
@@ -160,9 +160,9 @@ llvmCruxConfig = do
160160
laxConstantEquality <-
161161
Crux.section "lax-constant-equality" Crux.yesOrNoSpec False
162162
"Allow equality comparisons between pointers to constant data"
163-
readUnwrittenMemory <-
164-
Crux.section "read-unwritten-memory" Crux.yesOrNoSpec False
165-
"Allow reading from previously unwritten memory"
163+
laxLoadsAndStores <-
164+
Crux.section "lax-loads-and-stores" Crux.yesOrNoSpec False
165+
"Relax some of Crucible's validity checks for memory loads and stores"
166166
return MemOptions{..}
167167

168168
transOpts <- do laxArith <-

‎crux-llvm/test-data/golden/T783.config

-1
This file was deleted.

‎crux-llvm/test-data/golden/T783.c renamed to ‎crux-llvm/test-data/golden/T783a.c

File renamed without changes.

‎crux-llvm/test-data/golden/T783a.config

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
lax-loads-and-stores: yes

‎crux-llvm/test-data/golden/T783.good renamed to ‎crux-llvm/test-data/golden/T783a.good

File renamed without changes.

‎crux-llvm/test-data/golden/T783b.c

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
struct s {
2+
unsigned int a;
3+
unsigned int b;
4+
};
5+
6+
int f() {
7+
struct s *ss = malloc(sizeof(struct s));
8+
ss->b += 1;
9+
return ss->b;
10+
}
11+
12+
int main() {
13+
return f();
14+
}

‎crux-llvm/test-data/golden/T783b.config

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
lax-loads-and-stores: yes

‎crux-llvm/test-data/golden/T783b.good

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
[Crux] Overall status: Valid.

0 commit comments

Comments
 (0)