Skip to content

Commit 51c638c

Browse files
axelcool1234axelcool1234
committed
Move transfer functions
1 parent 5a8be37 commit 51c638c

2 files changed

Lines changed: 130 additions & 120 deletions

File tree

‎Veir/Analysis/DataFlow/Domains/KnownBitsDomain.lean‎

Lines changed: 1 addition & 105 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
module
22

33
public import Veir.Analysis.DataFlow.Domains.AbstractDomain
4-
public import Veir.Interpreter.Evaluate
4+
public import Veir.RuntimeValue
55
import Veir.Meta.BVDecide
66

77
public section
@@ -50,42 +50,6 @@ def join? (lhs rhs : KnownBits) : Option KnownBits :=
5050
else
5151
none
5252

53-
/-- Known bits produced by bitwise AND. -/
54-
def bitwiseAnd? (lhs rhs : KnownBits) : Option KnownBits :=
55-
if h : lhs.bitwidth = rhs.bitwidth then
56-
let rhsZero := h ▸ rhs.zero
57-
let rhsOne := h ▸ rhs.one
58-
some
59-
{ bitwidth := lhs.bitwidth
60-
zero := lhs.zero ||| rhsZero
61-
one := lhs.one &&& rhsOne }
62-
else
63-
none
64-
65-
/-- Known bits produced by bitwise OR. -/
66-
def bitwiseOr? (lhs rhs : KnownBits) : Option KnownBits :=
67-
if h : lhs.bitwidth = rhs.bitwidth then
68-
let rhsZero := h ▸ rhs.zero
69-
let rhsOne := h ▸ rhs.one
70-
some
71-
{ bitwidth := lhs.bitwidth
72-
zero := lhs.zero &&& rhsZero
73-
one := lhs.one ||| rhsOne }
74-
else
75-
none
76-
77-
/-- Known bits produced by bitwise XOR. -/
78-
def bitwiseXor? (lhs rhs : KnownBits) : Option KnownBits :=
79-
if h : lhs.bitwidth = rhs.bitwidth then
80-
let rhsZero := h ▸ rhs.zero
81-
let rhsOne := h ▸ rhs.one
82-
some
83-
{ bitwidth := lhs.bitwidth
84-
zero := (lhs.zero &&& rhsZero) ||| (lhs.one &&& rhsOne)
85-
one := (lhs.zero &&& rhsOne) ||| (lhs.one &&& rhsZero) }
86-
else
87-
none
88-
8953
end KnownBits
9054

9155
/--
@@ -196,74 +160,6 @@ def join : KnownBitsLattice → KnownBitsLattice → KnownBitsLattice
196160
instance : Join KnownBitsLattice where
197161
join := join
198162

199-
/-- Transfer known bits through bitwise AND. -/
200-
def bitwiseAnd : KnownBitsLattice → KnownBitsLattice → KnownBitsLattice
201-
| .bottom, _ | _, .bottom => .bottom
202-
| .top, .top => .top
203-
| .known lhs, .top | .top, .known lhs =>
204-
.known { lhs with one := 0 }
205-
| .known lhs, .known rhs =>
206-
match lhs.bitwiseAnd? rhs with
207-
| some bits => .known bits
208-
| none => .top
209-
210-
/--
211-
Known-bits AND soundly over-approximates every result produced by the LLVM
212-
interpreter from concrete values represented by its abstract operands.
213-
-/
214-
theorem bitwiseAnd_sound
215-
(lhs rhs : KnownBitsLattice)
216-
(bitwidth : Nat)
217-
(lhsValue rhsValue resultValue : BitVec bitwidth)
218-
(hlhs : RuntimeValue.int bitwidth (.val lhsValue) ∈ γ lhs)
219-
(hrhs : RuntimeValue.int bitwidth (.val rhsValue) ∈ γ rhs)
220-
(heval :
221-
foldEvaluate (.llvm .and) () #[IntegerType.mk bitwidth]
222-
#[.int bitwidth (.val lhsValue), .int bitwidth (.val rhsValue)] =
223-
.ok #[.int bitwidth (.val resultValue)]) :
224-
RuntimeValue.int bitwidth (.val resultValue) ∈ γ (bitwiseAnd lhs rhs) := by
225-
obtain rfl : resultValue = lhsValue &&& rhsValue := by
226-
simpa [foldEvaluate_llvm_and] using heval.symm
227-
cases lhs <;> cases rhs <;> simp_all only [not_mem_γ_bottom, mem_γ_top, bitwiseAnd]
228-
case known.top | top.known =>
229-
first
230-
| (obtain ⟨zero, _, rfl, hzero, _⟩ := mem_γ_known_iff.mp hlhs)
231-
| (obtain ⟨zero, _, rfl, hzero, _⟩ := mem_γ_known_iff.mp hrhs)
232-
refine mem_γ_known_iff.mpr
233-
⟨zero, 0, rfl, fun i hi h => by simp [hzero i hi h], by simp⟩
234-
case known.known =>
235-
obtain ⟨lhsZero, lhsOne, rfl, hlzero, hlone⟩ := mem_γ_known_iff.mp hlhs
236-
obtain ⟨rhsZero, rhsOne, rfl, hrzero, hrone⟩ := mem_γ_known_iff.mp hrhs
237-
simp only [KnownBits.bitwiseAnd?]
238-
refine mem_γ_known_iff.mpr
239-
⟨lhsZero ||| rhsZero, lhsOne &&& rhsOne, rfl, ?_,
240-
fun i hi h => by simp_all [hlone i hi, hrone i hi]⟩
241-
· intro i hi hresultZero
242-
specialize hlzero i hi
243-
specialize hrzero i hi
244-
simp_all <;> veir_bv_decide
245-
246-
/-- Transfer known bits through bitwise OR. -/
247-
def bitwiseOr : KnownBitsLattice → KnownBitsLattice → KnownBitsLattice
248-
| .bottom, _ | _, .bottom => .bottom
249-
| .top, .top => .top
250-
| .known lhs, .top | .top, .known lhs =>
251-
.known { lhs with zero := 0 }
252-
| .known lhs, .known rhs =>
253-
match lhs.bitwiseOr? rhs with
254-
| some bits => .known bits
255-
| none => .top
256-
257-
/-- Transfer known bits through bitwise XOR. -/
258-
def bitwiseXor : KnownBitsLattice → KnownBitsLattice → KnownBitsLattice
259-
| .bottom, _ | _, .bottom => .bottom
260-
| .top, .top => .top
261-
| .known lhs, .top | .top, .known lhs => .unknown lhs.bitwidth
262-
| .known lhs, .known rhs =>
263-
match lhs.bitwiseXor? rhs with
264-
| some bits => .known bits
265-
| none => .top
266-
267163
end KnownBitsLattice
268164

269165
end Veir

‎Veir/Analysis/DataFlow/KnownBitsAnalysis.lean‎

Lines changed: 129 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,10 @@ module
22

33
public import Veir.Analysis.DataFlow.Domains.KnownBitsDomain
44
public import Veir.Analysis.DataFlow.SparseForwardDataFlowAnalysis
5+
public import Veir.Interpreter.Evaluate
56

67
import Veir.Interfaces.FoldInterfaces
8+
import Veir.Meta.BVDecide
79

810
public section
911

@@ -18,6 +20,118 @@ operations in the Arith, Comb, and LLVM dialects. Other integer-producing operat
1820
conservatively produce an unknown value of the result width.
1921
-/
2022

23+
namespace KnownBits
24+
25+
/-- Known bits produced by bitwise AND. -/
26+
def bitwiseAnd? (lhs rhs : KnownBits) : Option KnownBits :=
27+
if h : lhs.bitwidth = rhs.bitwidth then
28+
let rhsZero := h ▸ rhs.zero
29+
let rhsOne := h ▸ rhs.one
30+
some
31+
{ bitwidth := lhs.bitwidth
32+
zero := lhs.zero ||| rhsZero
33+
one := lhs.one &&& rhsOne }
34+
else
35+
none
36+
37+
/-- Known bits produced by bitwise OR. -/
38+
def bitwiseOr? (lhs rhs : KnownBits) : Option KnownBits :=
39+
if h : lhs.bitwidth = rhs.bitwidth then
40+
let rhsZero := h ▸ rhs.zero
41+
let rhsOne := h ▸ rhs.one
42+
some
43+
{ bitwidth := lhs.bitwidth
44+
zero := lhs.zero &&& rhsZero
45+
one := lhs.one ||| rhsOne }
46+
else
47+
none
48+
49+
/-- Known bits produced by bitwise XOR. -/
50+
def bitwiseXor? (lhs rhs : KnownBits) : Option KnownBits :=
51+
if h : lhs.bitwidth = rhs.bitwidth then
52+
let rhsZero := h ▸ rhs.zero
53+
let rhsOne := h ▸ rhs.one
54+
some
55+
{ bitwidth := lhs.bitwidth
56+
zero := (lhs.zero &&& rhsZero) ||| (lhs.one &&& rhsOne)
57+
one := (lhs.zero &&& rhsOne) ||| (lhs.one &&& rhsZero) }
58+
else
59+
none
60+
61+
end KnownBits
62+
63+
namespace KnownBitsLattice
64+
65+
/-- Transfer known bits through bitwise AND. -/
66+
def bitwiseAnd : KnownBitsLattice → KnownBitsLattice → KnownBitsLattice
67+
| .bottom, _ | _, .bottom => .bottom
68+
| .top, .top => .top
69+
| .known lhs, .top | .top, .known lhs =>
70+
.known { lhs with one := 0 }
71+
| .known lhs, .known rhs =>
72+
match lhs.bitwiseAnd? rhs with
73+
| some bits => .known bits
74+
| none => .top
75+
76+
/--
77+
Known-bits AND soundly over-approximates every result produced by the LLVM
78+
interpreter from concrete values represented by its abstract operands.
79+
-/
80+
theorem bitwiseAnd_sound
81+
(lhs rhs : KnownBitsLattice)
82+
(bitwidth : Nat)
83+
(lhsValue rhsValue resultValue : BitVec bitwidth)
84+
(hlhs : RuntimeValue.int bitwidth (.val lhsValue) ∈ γ lhs)
85+
(hrhs : RuntimeValue.int bitwidth (.val rhsValue) ∈ γ rhs)
86+
(heval :
87+
foldEvaluate (.llvm .and) () #[IntegerType.mk bitwidth]
88+
#[.int bitwidth (.val lhsValue), .int bitwidth (.val rhsValue)] =
89+
.ok #[.int bitwidth (.val resultValue)]) :
90+
RuntimeValue.int bitwidth (.val resultValue) ∈ γ (bitwiseAnd lhs rhs) := by
91+
obtain rfl : resultValue = lhsValue &&& rhsValue := by
92+
simpa [foldEvaluate_llvm_and] using heval.symm
93+
cases lhs <;> cases rhs <;> simp_all only [not_mem_γ_bottom, mem_γ_top, bitwiseAnd]
94+
case known.top | top.known =>
95+
first
96+
| (obtain ⟨zero, _, rfl, hzero, _⟩ := mem_γ_known_iff.mp hlhs)
97+
| (obtain ⟨zero, _, rfl, hzero, _⟩ := mem_γ_known_iff.mp hrhs)
98+
refine mem_γ_known_iff.mpr
99+
⟨zero, 0, rfl, fun i hi h => by simp [hzero i hi h], by simp⟩
100+
case known.known =>
101+
obtain ⟨lhsZero, lhsOne, rfl, hlzero, hlone⟩ := mem_γ_known_iff.mp hlhs
102+
obtain ⟨rhsZero, rhsOne, rfl, hrzero, hrone⟩ := mem_γ_known_iff.mp hrhs
103+
simp only [KnownBits.bitwiseAnd?]
104+
refine mem_γ_known_iff.mpr
105+
⟨lhsZero ||| rhsZero, lhsOne &&& rhsOne, rfl, ?_,
106+
fun i hi h => by simp_all [hlone i hi, hrone i hi]⟩
107+
· intro i hi hresultZero
108+
specialize hlzero i hi
109+
specialize hrzero i hi
110+
simp_all <;> veir_bv_decide
111+
112+
/-- Transfer known bits through bitwise OR. -/
113+
def bitwiseOr : KnownBitsLattice → KnownBitsLattice → KnownBitsLattice
114+
| .bottom, _ | _, .bottom => .bottom
115+
| .top, .top => .top
116+
| .known lhs, .top | .top, .known lhs =>
117+
.known { lhs with zero := 0 }
118+
| .known lhs, .known rhs =>
119+
match lhs.bitwiseOr? rhs with
120+
| some bits => .known bits
121+
| none => .top
122+
123+
/-- Transfer known bits through bitwise XOR. -/
124+
def bitwiseXor : KnownBitsLattice → KnownBitsLattice → KnownBitsLattice
125+
| .bottom, _ | _, .bottom => .bottom
126+
| .top, .top => .top
127+
| .known lhs, .top | .top, .known lhs => .unknown lhs.bitwidth
128+
| .known lhs, .known rhs =>
129+
match lhs.bitwiseXor? rhs with
130+
| some bits => .known bits
131+
| none => .top
132+
133+
end KnownBitsLattice
134+
21135
namespace KnownBitsAnalysis
22136

23137
instance : SparseFactSpec .knownBits KnownBitsLattice where
@@ -26,10 +140,10 @@ instance : SparseFactSpec .knownBits KnownBitsLattice where
26140
private def transferBitwise
27141
(operation : KnownBitsLattice → KnownBitsLattice → KnownBitsLattice)
28142
(numResults : Nat)
29-
(operands : Array KnownBitsLattice) : Array (Option KnownBitsLattice) :=
143+
(operands : Array KnownBitsLattice) : Array KnownBitsLattice :=
30144
match operands.toList with
31-
| [] => Array.replicate numResults none
32-
| first :: rest => Array.replicate numResults (some (rest.foldl operation first))
145+
| [] => Array.replicate numResults ⊥
146+
| first :: rest => Array.replicate numResults (rest.foldl operation first)
33147

34148
/--
35149
Infer known bits for one operation. Bottom operands cause the transfer to wait for
@@ -38,18 +152,18 @@ more information; unsupported integer results receive a width-aware unknown valu
38152
def transfer
39153
(op : OperationPtr)
40154
(operands : Array KnownBitsLattice)
41-
(irCtx : WfIRContext OpCode) : Array (Option KnownBitsLattice) :=
155+
(irCtx : WfIRContext OpCode) : Array KnownBitsLattice :=
42156
let numResults := op.getNumResults! irCtx.raw
43157
let resultTypes := op.getResultTypes! irCtx.raw
44158
let pessimisticUpdates := resultTypes.map fun resultType =>
45159
match resultType.val with
46-
| .integerType intType => some (.unknown intType.bitwidth)
47-
| _ => none
160+
| .integerType intType => .unknown intType.bitwidth
161+
| _ => ⊥
48162

49163
if op.getNumRegions! irCtx.raw ≠ 0 then
50164
pessimisticUpdates
51165
else if operands.any (· = ⊥) then
52-
Array.replicate numResults none
166+
Array.replicate numResults ⊥
53167
else
54168
let opType := op.getOpType! irCtx.raw
55169
let exactOperands := operands.map fun
@@ -63,31 +177,31 @@ def transfer
63177
| some results =>
64178
(results.zip resultTypes).map fun (result, resultType) =>
65179
match resultType.val, result with
66-
| .integerType _, .useOperand index => some (operands[index]?.getD ⊤)
180+
| .integerType _, .useOperand index => operands[index]?.getD ⊤
67181
| .integerType intType, .useConstant (.int bitwidth (.val value)) =>
68182
if h : bitwidth = intType.bitwidth then
69183
let value := value.cast h
70-
some (.known { bitwidth := intType.bitwidth, zero := ~~~value, one := value })
184+
.known { bitwidth := intType.bitwidth, zero := ~~~value, one := value }
71185
else
72-
some ⊤
73-
| .integerType _, .useConstant _ => some ⊤
74-
| _, _ => none
186+
⊤
187+
| .integerType _, .useConstant _ => ⊤
188+
| _, _ => ⊥
75189
| none =>
76190
match opType with
77191
| OpCode.arith Arith.constant =>
78192
let props := op.getProperties! irCtx.raw (OpCode.arith Arith.constant)
79193
Array.replicate numResults
80-
(some (.constant props.value.type.bitwidth props.value.value))
194+
(.constant props.value.type.bitwidth props.value.value)
81195
| OpCode.llvm Llvm.mlir__constant =>
82196
let props := op.getProperties! irCtx.raw (OpCode.llvm Llvm.mlir__constant)
83197
match props.value with
84198
| .integer attr =>
85-
Array.replicate numResults (some (.constant attr.type.bitwidth attr.value))
199+
Array.replicate numResults (.constant attr.type.bitwidth attr.value)
86200
| _ => pessimisticUpdates
87201
| OpCode.hw HW.constant =>
88202
let props := op.getProperties! irCtx.raw (OpCode.hw HW.constant)
89203
Array.replicate numResults
90-
(some (.constant props.value.type.bitwidth props.value.value))
204+
(.constant props.value.type.bitwidth props.value.value)
91205
| OpCode.arith Arith.andi
92206
| OpCode.llvm Llvm.and
93207
| OpCode.comb Comb.and =>

0 commit comments

Comments
 (0)