Skip to content

Commit 5d6e42e

Browse files
tobiasgrossertobiasgrosser
authored
chore(LLVM): split files in Basic and Lemmas (#1478)
Separating definitions and theorems should make the code easier to navigate.
1 parent 635c263 commit 5d6e42e

3 files changed

Lines changed: 114 additions & 91 deletions

File tree

‎Veir/Data/LLVM/Ptr.lean‎

Lines changed: 2 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -1,93 +1,4 @@
11
module
22

3-
public import Veir.Data.LLVM.Byte.Basic
4-
5-
import all Veir.Data.LLVM.Int.Bitblast
6-
import all Veir.Data.LLVM.Byte.Basic
7-
8-
namespace Veir.Data.LLVM
9-
10-
public section
11-
12-
/--
13-
A pointer-typed value: an address, or poison.
14-
15-
We currently model a 64-bit system.
16-
-/
17-
inductive Ptr where
18-
/-- An address. -/
19-
| val (p : UInt64)
20-
/-- A poison value indicating deferred undefined behavior. -/
21-
| poison
22-
deriving Inhabited, Repr, DecidableEq
23-
24-
namespace Ptr
25-
26-
def null : Ptr := .val 0
27-
28-
@[expose, simp, grind .]
29-
def isRefinedBy : Ptr → Ptr → Prop
30-
| .poison, _ => True
31-
| .val p, .val p' => p = p'
32-
| .val _, .poison => False
33-
34-
@[inherit_doc] infix:50 " ⊒ " => LLVM.Ptr.isRefinedBy
35-
36-
@[simp, grind .]
37-
theorem isRefinedBy_refl (p : Ptr) : p ⊒ p := by
38-
cases p <;> simp
39-
40-
@[grind .]
41-
theorem isRefinedBy_trans {p₁ p₂ p₃ : Ptr}
42-
(h12 : p₁ ⊒ p₂) (h23 : p₂ ⊒ p₃) : p₁ ⊒ p₃ := by
43-
cases p₁ <;> cases p₂ <;> cases p₃ <;> simp_all
44-
45-
/-- Only the same pointer refines a pointer that is not poison. -/
46-
@[grind .]
47-
theorem eq_of_val_isRefinedBy {p : UInt64} {q : Ptr}
48-
(h : Ptr.val p ⊒ q) : q = .val p := by
49-
cases q <;> simp_all
50-
51-
@[simp, grind =]
52-
def toInt (p : Ptr) : Int 64 :=
53-
match p with
54-
| .val p => .val p.toBitVec
55-
| .poison => .poison
56-
57-
@[simp, grind =]
58-
def ofInt (i : Int 64) : Ptr :=
59-
match i with
60-
| .val v => .val (UInt64.ofBitVec v)
61-
| .poison => .poison
62-
63-
@[simp, grind =]
64-
theorem ofInt_toInt (p : Ptr) : ofInt p.toInt = p := by
65-
cases p <;> simp
66-
67-
@[simp, grind =]
68-
theorem toInt_ofInt (i : Int 64) : (ofInt i).toInt = i := by
69-
cases i <;> simp
70-
71-
/-- The pointer whose bits are `b`, poison if any bit is poison. -/
72-
def ofByte (b : Byte 64) : Ptr := ofInt b.toInt
73-
74-
/-- The bits of a pointer: all poison for a poison pointer. -/
75-
def toByte (p : Ptr) : Byte 64 := Byte.fromInt p.toInt
76-
77-
@[simp, grind =]
78-
theorem ofByte_toByte (p : Ptr) : ofByte p.toByte = p := by
79-
cases p <;> simp [ofByte, toByte, Byte.toInt, Byte.fromInt, Int.isPoison, Int.getValue]
80-
81-
/-- Prints as `ptr(0x…)`, so a pointer is told apart from an integer in program output. -/
82-
instance : ToString Ptr where
83-
toString
84-
| .val p =>
85-
let digits := String.ofList (Nat.toDigits 16 p.toNat)
86-
s!"ptr(0x{"".pushn '0' (16 - digits.length) ++ digits})"
87-
| .poison => "poison"
88-
89-
end Ptr
90-
91-
end
92-
93-
end Veir.Data.LLVM
3+
public import Veir.Data.LLVM.Ptr.Basic
4+
public import Veir.Data.LLVM.Ptr.Lemmas

‎Veir/Data/LLVM/Ptr/Basic.lean‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
module
2+
3+
public import Veir.Data.LLVM.Byte.Basic
4+
5+
namespace Veir.Data.LLVM
6+
7+
public section
8+
9+
/--
10+
A pointer-typed value: an address, or poison.
11+
12+
We currently model a 64-bit system.
13+
-/
14+
inductive Ptr where
15+
/-- An address. -/
16+
| val (p : UInt64)
17+
/-- A poison value indicating deferred undefined behavior. -/
18+
| poison
19+
deriving Inhabited, Repr, DecidableEq
20+
21+
namespace Ptr
22+
23+
def null : Ptr := .val 0
24+
25+
@[expose, simp, grind .]
26+
def isRefinedBy : Ptr → Ptr → Prop
27+
| .poison, _ => True
28+
| .val p, .val p' => p = p'
29+
| .val _, .poison => False
30+
31+
@[inherit_doc] infix:50 " ⊒ " => LLVM.Ptr.isRefinedBy
32+
33+
/-- The address as a 64-bit integer; poison for a poison pointer. -/
34+
@[simp, grind =]
35+
def toInt (p : Ptr) : Int 64 :=
36+
match p with
37+
| .val p => .val p.toBitVec
38+
| .poison => .poison
39+
40+
/-- The pointer at address `i`; poison for poison. -/
41+
@[simp, grind =]
42+
def ofInt (i : Int 64) : Ptr :=
43+
match i with
44+
| .val v => .val (UInt64.ofBitVec v)
45+
| .poison => .poison
46+
47+
/-- The pointer whose bits are `b`, poison if any bit is poison. -/
48+
def ofByte (b : Byte 64) : Ptr := ofInt b.toInt
49+
50+
/-- The bits of a pointer: all poison for a poison pointer. -/
51+
def toByte (p : Ptr) : Byte 64 := Byte.fromInt p.toInt
52+
53+
/-- Prints as `ptr(0x…)`, so a pointer is told apart from an integer in program output. -/
54+
instance : ToString Ptr where
55+
toString
56+
| .val p =>
57+
let digits := String.ofList (Nat.toDigits 16 p.toNat)
58+
s!"ptr(0x{"".pushn '0' (16 - digits.length) ++ digits})"
59+
| .poison => "poison"
60+
61+
end Ptr
62+
63+
end
64+
65+
end Veir.Data.LLVM

‎Veir/Data/LLVM/Ptr/Lemmas.lean‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
module
2+
3+
public import Veir.Data.LLVM.Ptr.Basic
4+
import all Veir.Data.LLVM.Ptr.Basic
5+
import all Veir.Data.LLVM.Int.Bitblast
6+
import all Veir.Data.LLVM.Byte.Basic
7+
8+
namespace Veir.Data.LLVM.Ptr
9+
10+
public section
11+
12+
/- # isRefinedBy -/
13+
14+
@[simp, grind .]
15+
theorem isRefinedBy_refl (p : Ptr) : p ⊒ p := by
16+
cases p <;> simp
17+
18+
@[grind .]
19+
theorem isRefinedBy_trans {p₁ p₂ p₃ : Ptr}
20+
(h12 : p₁ ⊒ p₂) (h23 : p₂ ⊒ p₃) : p₁ ⊒ p₃ := by
21+
cases p₁ <;> cases p₂ <;> cases p₃ <;> simp_all
22+
23+
/-- Only the same pointer refines a pointer that is not poison. -/
24+
@[grind .]
25+
theorem eq_of_val_isRefinedBy {p : UInt64} {q : Ptr}
26+
(h : Ptr.val p ⊒ q) : q = .val p := by
27+
cases q <;> simp_all
28+
29+
/- # {to,of}Int -/
30+
31+
@[simp, grind =]
32+
theorem ofInt_toInt (p : Ptr) : ofInt p.toInt = p := by
33+
cases p <;> simp
34+
35+
@[simp, grind =]
36+
theorem toInt_ofInt (i : Int 64) : (ofInt i).toInt = i := by
37+
cases i <;> simp
38+
39+
/- # {to,of}Byte -/
40+
41+
@[simp, grind =]
42+
theorem ofByte_toByte (p : Ptr) : ofByte p.toByte = p := by
43+
cases p <;> simp [ofByte, toByte, Byte.toInt, Byte.fromInt, Int.isPoison, Int.getValue]
44+
45+
end
46+
47+
end Veir.Data.LLVM.Ptr

0 commit comments

Comments
 (0)