Skip to content

Commit c07213c

Browse files
langston-barrettlangston-barrett
authored
Merge pull request #931 from GaloisInc/lb/bug
uc-crux-llvm: Improve tracking of unclassified errors
2 parents 2daf99d + aa648cc commit c07213c

File tree

9 files changed

+330
-103
lines changed

9 files changed

+330
-103
lines changed

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

+6
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ module Lang.Crucible.LLVM.MemModel.Pointer
4545
, llvmPointerView
4646
, llvmPointerBlock
4747
, llvmPointerOffset
48+
, llvmPointerType
4849
, muxLLVMPtr
4950
, llvmPointer_bv
5051
, mkNullPointer
@@ -114,6 +115,11 @@ llvmPointerBlock (LLVMPointer blk _) = blk
114115
llvmPointerOffset :: LLVMPtr sym w -> SymBV sym w
115116
llvmPointerOffset (LLVMPointer _ off) = off
116117

118+
llvmPointerType :: IsExpr (SymExpr sym) => LLVMPtr sym w -> TypeRepr (LLVMPointerType w)
119+
llvmPointerType ptr =
120+
case exprType (llvmPointerOffset ptr) of
121+
BaseBVRepr w -> LLVMPointerRepr w
122+
117123
-- | Type family defining how @LLVMPointerType@ unfolds.
118124
type family LLVMPointerImpl sym ctx where
119125
LLVMPointerImpl sym (EmptyCtx ::> BVType w) = LLVMPointer sym w

‎uc-crux-llvm/src/UCCrux/LLVM/Bug.hs

+103
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
{-
2+
Module : UCCrux.LLVM.Bug
3+
Description : Representation of possible bugs
4+
Copyright : (c) Galois, Inc 2021
5+
License : BSD3
6+
Maintainer : Langston Barrett <[email protected]>
7+
Stability : provisional
8+
-}
9+
10+
{-# LANGUAGE FlexibleContexts #-}
11+
{-# LANGUAGE LambdaCase #-}
12+
{-# LANGUAGE GADTs #-}
13+
{-# LANGUAGE PolyKinds #-}
14+
15+
module UCCrux.LLVM.Bug
16+
( Bug,
17+
bugBehavior,
18+
bugLoc,
19+
makeBug,
20+
ppBug,
21+
BugBehavior(..),
22+
ppBugBehavior,
23+
UndefinedBehaviorTag,
24+
getUndefinedBehaviorTag,
25+
makeUndefinedBehaviorTag,
26+
)
27+
where
28+
29+
{- ORMOLU_DISABLE -}
30+
import qualified Prettyprinter as PP
31+
32+
import What4.Interface (IsExpr, SymExpr)
33+
import qualified What4.ProgramLoc as What4
34+
35+
import Lang.Crucible.LLVM.MemModel.CallStack (CallStack, ppCallStack)
36+
import Lang.Crucible.LLVM.Errors (BadBehavior)
37+
import qualified Lang.Crucible.LLVM.Errors as LLVMErrors
38+
import Lang.Crucible.LLVM.Errors.MemoryError (MemoryErrorReason)
39+
import qualified Lang.Crucible.LLVM.Errors.MemoryError as MemErrors
40+
import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
41+
42+
import UCCrux.LLVM.Bug.UndefinedBehaviorTag (UndefinedBehaviorTag, getUndefinedBehaviorTag, makeUndefinedBehaviorTag)
43+
import UCCrux.LLVM.PP (ppProgramLoc)
44+
{- ORMOLU_ENABLE -}
45+
46+
-- | This is different from 'Lang.Crucible.LLVM.Errors.BadBehavior' in that
47+
-- it stores less data.
48+
data BugBehavior
49+
= BBUndefinedBehaviorTag !UndefinedBehaviorTag
50+
| BBMemoryErrorReason !MemoryErrorReason
51+
deriving (Eq, Ord)
52+
53+
ppBugBehavior :: BugBehavior -> PP.Doc ann
54+
ppBugBehavior =
55+
\case
56+
BBUndefinedBehaviorTag ub -> UB.explain (getUndefinedBehaviorTag ub)
57+
BBMemoryErrorReason mer -> MemErrors.ppMemoryErrorReason mer
58+
59+
instance PP.Pretty BugBehavior where
60+
pretty = ppBugBehavior
61+
62+
-- | A possible bug: What it is, and where it can occur.
63+
data Bug =
64+
Bug
65+
{ bugBehavior :: !BugBehavior
66+
, bugLoc :: !What4.ProgramLoc
67+
, bugCallStack :: !CallStack
68+
}
69+
deriving (Eq, Ord)
70+
71+
makeBug ::
72+
IsExpr (SymExpr sym) =>
73+
BadBehavior sym ->
74+
What4.ProgramLoc ->
75+
CallStack ->
76+
Bug
77+
makeBug bb loc callStack =
78+
Bug
79+
{ bugBehavior =
80+
case bb of
81+
LLVMErrors.BBUndefinedBehavior ub ->
82+
BBUndefinedBehaviorTag (makeUndefinedBehaviorTag ub)
83+
LLVMErrors.BBMemoryError (MemErrors.MemoryError _ rsn) ->
84+
BBMemoryErrorReason rsn,
85+
bugLoc = loc,
86+
bugCallStack = callStack
87+
}
88+
89+
ppBug :: Bug -> PP.Doc ann
90+
ppBug (Bug bb loc callStack) =
91+
PP.vsep
92+
[ ppBugBehavior bb
93+
, PP.pretty "at" <> PP.pretty (ppProgramLoc loc)
94+
, PP.pretty "in context:"
95+
, PP.indent 2 (ppCallStack callStack)
96+
]
97+
98+
-- | Non-lawful instance, only to be used in tests.
99+
instance Show Bug where
100+
show = show . ppBug
101+
102+
instance PP.Pretty Bug where
103+
pretty = ppBug

‎uc-crux-llvm/src/UCCrux/LLVM/Bug/UndefinedBehaviorTag.hs

+165
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
1+
{-
2+
Module : UCCrux.LLVM.Bug.UndefinedBehaviorTag
3+
Description : Representation of undefined behavior
4+
Copyright : (c) Galois, Inc 2021
5+
License : BSD3
6+
Maintainer : Langston Barrett <[email protected]>
7+
Stability : provisional
8+
-}
9+
10+
{-# LANGUAGE GADTs #-}
11+
{-# LANGUAGE FlexibleContexts #-}
12+
{-# LANGUAGE LambdaCase #-}
13+
14+
module UCCrux.LLVM.Bug.UndefinedBehaviorTag
15+
( UndefinedBehaviorTag,
16+
getUndefinedBehaviorTag,
17+
makeUndefinedBehaviorTag,
18+
)
19+
where
20+
21+
{- ORMOLU_DISABLE -}
22+
import Data.Type.Equality (testEquality)
23+
24+
import Lang.Crucible.Simulator.RegValue (RegValue'(unRV))
25+
import Lang.Crucible.Types (BVType, TypeRepr, baseToType)
26+
27+
import Data.Parameterized.Classes (compareF)
28+
import Data.Parameterized.ClassesC (testEqualityC, compareC)
29+
30+
import What4.Interface (IsExpr, SymExpr, exprType)
31+
32+
import Lang.Crucible.LLVM.Errors.Poison (Poison(..))
33+
import Lang.Crucible.LLVM.Errors.UndefinedBehavior (UndefinedBehavior(..))
34+
import Lang.Crucible.LLVM.MemModel.Pointer (LLVMPointerType, llvmPointerType)
35+
{- ORMOLU_ENABLE -}
36+
37+
-- | A simplification of 'UndefinedBehavior' that keeps less information around.
38+
-- Used for deduplicating reports about possible bugs/errors in programs and
39+
-- explaining the provenance of inferred function preconditions.
40+
newtype UndefinedBehaviorTag =
41+
UndefinedBehaviorTag { getUndefinedBehaviorTag :: UndefinedBehavior TypeRepr }
42+
43+
makeUndefinedBehaviorTag ::
44+
IsExpr (SymExpr sym) =>
45+
UndefinedBehavior (RegValue' sym) ->
46+
UndefinedBehaviorTag
47+
makeUndefinedBehaviorTag =
48+
UndefinedBehaviorTag .
49+
\case
50+
FreeBadOffset ptr ->
51+
FreeBadOffset (pointer ptr)
52+
FreeUnallocated ptr ->
53+
FreeUnallocated (pointer ptr)
54+
DoubleFree ptr ->
55+
DoubleFree (pointer ptr)
56+
MemsetInvalidRegion ptr val len ->
57+
MemsetInvalidRegion (pointer ptr) (bv val) (bv len)
58+
ReadBadAlignment ptr a ->
59+
ReadBadAlignment (pointer ptr) a
60+
WriteBadAlignment ptr a ->
61+
WriteBadAlignment (pointer ptr) a
62+
PtrAddOffsetOutOfBounds ptr off ->
63+
PtrAddOffsetOutOfBounds (pointer ptr) (bv off)
64+
CompareInvalidPointer op p1 p2 ->
65+
CompareInvalidPointer op (pointer p1) (pointer p2)
66+
CompareDifferentAllocs p1 p2 ->
67+
CompareDifferentAllocs (pointer p1) (pointer p2)
68+
PtrSubDifferentAllocs p1 p2 ->
69+
PtrSubDifferentAllocs (pointer p1) (pointer p2)
70+
PointerFloatCast ptr tp ->
71+
PointerFloatCast (pointer ptr) tp
72+
PointerIntCast ptr tp ->
73+
PointerIntCast (pointer ptr) tp
74+
PointerUnsupportedOp ptr msg ->
75+
PointerUnsupportedOp (pointer ptr) msg
76+
ComparePointerToBV ptr val ->
77+
ComparePointerToBV (pointer ptr) (bv val)
78+
UDivByZero v1 v2 ->
79+
UDivByZero (bv v1) (bv v2)
80+
SDivByZero v1 v2 ->
81+
SDivByZero (bv v1) (bv v2)
82+
URemByZero v1 v2 ->
83+
URemByZero (bv v1) (bv v2)
84+
SRemByZero v1 v2 ->
85+
SRemByZero (bv v1) (bv v2)
86+
SDivOverflow v1 v2 ->
87+
SDivOverflow (bv v1) (bv v2)
88+
SRemOverflow v1 v2 ->
89+
SRemOverflow (bv v1) (bv v2)
90+
AbsIntMin v ->
91+
AbsIntMin (bv v)
92+
PoisonValueCreated p ->
93+
PoisonValueCreated (poison p)
94+
where
95+
pointer ::
96+
IsExpr (SymExpr sym) =>
97+
RegValue' sym (LLVMPointerType w) ->
98+
TypeRepr (LLVMPointerType w)
99+
pointer = llvmPointerType . unRV
100+
101+
bv ::
102+
IsExpr (SymExpr sym) =>
103+
RegValue' sym (BVType w) ->
104+
TypeRepr (BVType w)
105+
bv = baseToType . exprType . unRV
106+
107+
poison ::
108+
IsExpr (SymExpr sym) =>
109+
Poison (RegValue' sym) ->
110+
Poison TypeRepr
111+
poison =
112+
\case
113+
AddNoUnsignedWrap v1 v2 ->
114+
AddNoUnsignedWrap (bv v1) (bv v2)
115+
AddNoSignedWrap v1 v2 ->
116+
AddNoSignedWrap (bv v1) (bv v2)
117+
SubNoUnsignedWrap v1 v2 ->
118+
SubNoUnsignedWrap (bv v1) (bv v2)
119+
SubNoSignedWrap v1 v2 ->
120+
SubNoSignedWrap (bv v1) (bv v2)
121+
MulNoUnsignedWrap v1 v2 ->
122+
MulNoUnsignedWrap(bv v1) (bv v2)
123+
MulNoSignedWrap v1 v2 ->
124+
MulNoSignedWrap (bv v1) (bv v2)
125+
UDivExact v1 v2 ->
126+
UDivExact (bv v1) (bv v2)
127+
SDivExact v1 v2 ->
128+
SDivExact (bv v1) (bv v2)
129+
ShlOp2Big v1 v2 ->
130+
ShlOp2Big (bv v1) (bv v2)
131+
ShlNoUnsignedWrap v1 v2 ->
132+
ShlNoUnsignedWrap (bv v1) (bv v2)
133+
ShlNoSignedWrap v1 v2 ->
134+
ShlNoSignedWrap (bv v1) (bv v2)
135+
LshrExact v1 v2 ->
136+
LshrExact (bv v1) (bv v2)
137+
LshrOp2Big v1 v2 ->
138+
LshrOp2Big (bv v1) (bv v2)
139+
AshrExact v1 v2 ->
140+
AshrExact (bv v1) (bv v2)
141+
AshrOp2Big v1 v2 ->
142+
AshrOp2Big (bv v1) (bv v2)
143+
ExtractElementIndex v ->
144+
ExtractElementIndex (bv v)
145+
InsertElementIndex v ->
146+
InsertElementIndex (bv v)
147+
GEPOutOfBounds p v ->
148+
GEPOutOfBounds (pointer p) (bv v)
149+
LLVMAbsIntMin v ->
150+
LLVMAbsIntMin (bv v)
151+
152+
-- | This instance is a coarsening of that for 'UndefinedBehavior'. In
153+
-- particular, there may be instances of 'UndefinedBehavior' that do not compare
154+
-- equal, but their projections under 'makeUndefinedBehaviorTag' do compare
155+
-- equal.
156+
instance Eq UndefinedBehaviorTag where
157+
UndefinedBehaviorTag t1 == UndefinedBehaviorTag t2 =
158+
testEqualityC testEquality t1 t2
159+
160+
-- | See comment on 'Eq'.
161+
--
162+
-- Under the hood, this uses 'unsafeCoerce'.
163+
instance Ord UndefinedBehaviorTag where
164+
compare (UndefinedBehaviorTag t1) (UndefinedBehaviorTag t2) =
165+
compareC compareF t1 t2

0 commit comments

Comments
 (0)