Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
118 commits
Select commit Hold shift + click to select a range
7e5a0dd
Parse relocatable file (hacky handling of relocations)
maturvo Jan 2, 2025
ecb6af3
Update config
maturvo Jan 3, 2025
7514a8a
Symbolic symbol table
maturvo Jan 4, 2025
58091d7
Convert to symbolic addresses to make things compile
maturvo Jan 4, 2025
03ce63b
DIsable typing
maturvo Jan 4, 2025
2614846
Refactor (symbolic) address to separate module
maturvo Jan 5, 2025
fd2c3ff
Symbolic runner (TODO parsing symbolic addresses from SMT)
maturvo Jan 5, 2025
d42ecf0
Run relocatable file
maturvo Jan 5, 2025
fbd7c07
Enable typer
maturvo Jan 6, 2025
49ffe70
Some debug prints
maturvo Jan 7, 2025
3f0498b
Mark potential bug
maturvo Jan 7, 2025
e4485cd
Add TODO
maturvo Jan 7, 2025
4ef12a1
Implement opcodes with relocations
maturvo Jan 7, 2025
8dd5040
[WIP] read relocations from linksem
maturvo Jan 7, 2025
d11e65a
[WIP] relocations from linksem
maturvo Jan 8, 2025
8d1db3e
WIP instructions with relocations
maturvo Jan 8, 2025
8722715
WIP
maturvo Jan 9, 2025
2d5379f
[WIP] symbolic traces
maturvo Jan 9, 2025
36f7741
Store segments with instruction
maturvo Jan 10, 2025
90b3ac8
WIP eval relocations
maturvo Jan 10, 2025
34824b1
Symbolic section addresses
maturvo Jan 12, 2025
897e638
Fix cache
maturvo Jan 12, 2025
88cb340
Make PC symbolic in isla
maturvo Jan 14, 2025
ebf0b27
Symbolic PC
maturvo Jan 14, 2025
dde2e98
WIP
maturvo Jan 15, 2025
516f4f1
wip
maturvo Jan 15, 2025
3832eb4
todo
maturvo Jan 15, 2025
83414d1
Smarter context full simplifier
maturvo Jan 16, 2025
75185ee
Simplify relocated addresses
maturvo Jan 16, 2025
ad13b15
Fix immediate encoding
maturvo Jan 17, 2025
1742403
Write with section offset
maturvo Jan 17, 2025
f3468d4
Fix type of pc values in state tree
maturvo Jan 17, 2025
8d417e6
Symbolic write
maturvo Jan 17, 2025
9cb38f4
Separate fragments for sections
maturvo Jan 20, 2025
7e10b1d
Initialise symvbols
maturvo Jan 20, 2025
9d5173e
Fix loading relocations
maturvo Jan 20, 2025
04e3bc6
Handle jumps
maturvo Jan 21, 2025
646f6a5
Convert dwarf from linksem
maturvo Jan 26, 2025
6f086f2
[wip] symbolic analyse
maturvo Jan 26, 2025
1424297
[wip] symbolic analyse
maturvo Jan 27, 2025
1d1611f
[wip] symbolic analyse
maturvo Jan 27, 2025
04ee90e
Fix parsing objdump
maturvo Jan 27, 2025
5d01030
notes
maturvo Jan 30, 2025
65ebed5
set SCTLR_EL2
maturvo Jan 30, 2025
d30207d
Make funcRD work
maturvo Jan 30, 2025
b0dc540
Fix init of large objects
maturvo Jan 31, 2025
bda07fb
[wip] Run program
maturvo Jan 31, 2025
8b30d35
Run and print debug info
maturvo Feb 1, 2025
7c5fd5f
Fix ldst relocations
maturvo Feb 1, 2025
84798b3
Fix rngmap croping
maturvo Feb 5, 2025
688d539
Fix symbolic bytes sub
maturvo Feb 5, 2025
a9b1c22
Eval debug variable expressions
maturvo Feb 5, 2025
02cf601
Nicer print (needs testing)
maturvo Feb 5, 2025
81d0dec
nicer print
maturvo Feb 15, 2025
83f1d45
Take state init function as arg in Run.Func
maturvo Feb 15, 2025
7ad0590
Make Sums.split sound
maturvo Feb 15, 2025
9430446
Context simplifier for relocation
maturvo Feb 25, 2025
27b4daf
Fix caching
maturvo Mar 18, 2025
65eb0ae
Refactor: use get_state_tree in run_prog
maturvo Mar 18, 2025
f025a7c
Update for changes in linksem
maturvo Apr 9, 2025
a212415
Test script
maturvo Apr 10, 2025
a77a87b
Fix rodata
maturvo Apr 10, 2025
c5e2b56
Fix loading objects
maturvo Apr 10, 2025
2bc6c01
Fix reading rodata
maturvo Apr 10, 2025
c1c5cc5
Multiple rodata sections
maturvo Apr 10, 2025
1ed0c5c
Generate section address constraints
maturvo Apr 10, 2025
65a7e04
Fix nondet
maturvo Apr 11, 2025
9c760c0
Fix symbolic bytes subranges
maturvo Apr 11, 2025
63d3ebb
Hack addres-size extract of constexpr
maturvo Apr 11, 2025
34b6c32
Testing: Warn about read variables
maturvo Apr 11, 2025
d65c184
More typer hacking
maturvo Apr 11, 2025
af5e7fe
Better section asserts
maturvo Apr 14, 2025
22996d3
Better logs
maturvo Apr 14, 2025
0cf6b06
Fix provenance with section fragments
maturvo Apr 14, 2025
1f25a8f
Make fbreg locations work
maturvo Apr 24, 2025
0ff8cc9
Fix read rodata
maturvo Apr 27, 2025
38f9e11
Fix printing execution
maturvo Apr 27, 2025
19343af
Nicer visualization
maturvo Apr 30, 2025
e66ab9c
Allow relocations in rodata and fix endianness problems
maturvo May 1, 2025
0f9393a
Remove print
maturvo May 1, 2025
6524a9d
Fix debug loc parsing
maturvo May 1, 2025
2feb3a6
Add sections non-overlap constraints
maturvo May 2, 2025
cfa543e
debug
maturvo May 3, 2025
e9ca185
More relocation types
maturvo May 3, 2025
d72240d
new relocation representation in linksem
maturvo May 3, 2025
f2f1d24
rename relocation assertions to checks
maturvo May 3, 2025
cd6e5a8
rm notes-TODO
maturvo May 3, 2025
1ce15b0
Merge pull request #1 from maturvo/evaluate
maturvo May 3, 2025
1fa15c3
Simrel (#2)
maturvo May 13, 2025
0d7f6b1
Fix analyse (#3)
maturvo May 13, 2025
d93683b
Merge pull request #18 from maturvo/master
PeterSewell Jun 14, 2025
1155731
fix syntax for parsing objdump with %-separated relocations
PeterSewell Jun 14, 2025
43d8f0a
Fix loading files
maturvo Jul 9, 2025
b5b2700
wip
maturvo Jul 9, 2025
ab8fb02
Parse both executable and relocatable files
maturvo Jul 10, 2025
a69e2d0
Allow both absolute and section-relative addresses (wip)
maturvo Jul 10, 2025
c10e465
Executor: accept absolute pc address
maturvo Jul 10, 2025
1cafb80
remove old todos
maturvo Jul 20, 2025
6a6fee9
Enable run-instr
maturvo Jul 20, 2025
320f764
Allow parsing absolute addresses
maturvo Jul 20, 2025
34cbb38
Comment on bit sizes used by relocation expressions
maturvo Jul 20, 2025
9a414ea
Use 0 as initial last_pc value (less ambiguous)
maturvo Jul 21, 2025
e8166a6
Resolve TODO
maturvo Jul 21, 2025
97e188a
Reloc byte seq
maturvo Jul 21, 2025
b0efce6
Use RelocByteSeq
maturvo Jul 31, 2025
da3095e
Use RelocBytesSeq in Elf.Segment
maturvo Jul 31, 2025
935547d
Enable run-bb
maturvo Jul 31, 2025
ed23d3d
Remove leftover debugging stuff
maturvo Jul 31, 2025
92ef1a6
cleanup todo
maturvo Jul 31, 2025
db289a0
Rename sections -> relocatable_sections and clarify its usage
maturvo Jul 31, 2025
a84ce4c
Reintroduce global fragment for all ELF sections
maturvo Jul 31, 2025
652931b
Fix form of PC value
maturvo Jul 31, 2025
85b24f7
Fix: stop emiting error about values being typed constexpr
maturvo Jul 31, 2025
d9fb48a
Allow running isla test with relocations
maturvo Aug 2, 2025
16d01d1
Remove "horrible hack"
maturvo Aug 12, 2025
a0aada1
Warn about weird lines in objdump
maturvo Aug 12, 2025
f7a5691
add nm to isla_aarch64.toml, following isla/configs/armv8p5.toml
PeterSewell Aug 15, 2025
af9d06a
wib
PeterSewell Aug 15, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,4 @@ _build/*
**/.merlin
test_asm/build
.rdcache
.vscode
2 changes: 1 addition & 1 deletion doc/html/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>index</title>
<link rel="stylesheet" href="./odoc.css"/>
<link rel="stylesheet" href="./odoc.support/odoc.css"/>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width,initial-scale=1.0"/>
</head>
Expand Down
2 changes: 1 addition & 1 deletion doc/html/read-dwarf/Analyse/Base/index.html
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Base (read-dwarf.Analyse.Base)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">read-dwarf</a> &#x00BB; <a href="../index.html">Analyse</a> &#x00BB; Base</nav><h1>Module <code>Analyse.Base</code></h1></header><dl><dt class="spec value" id="val-process_file"><a href="#val-process_file" class="anchor"></a><code><span class="keyword">val</span> process_file : unit <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Base (read-dwarf.Analyse.Base)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 3.0.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">Index</a> &#x00BB; <a href="../../index.html">read-dwarf</a> &#x00BB; <a href="../index.html">Analyse</a> &#x00BB; Base</nav><header class="odoc-preamble"><h1>Module <code><span>Analyse.Base</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-process_file"><a href="#val-process_file" class="anchor"></a><code><span><span class="keyword">val</span> process_file : <span>unit <span class="arrow">&#45;&gt;</span></span> unit</span></code></div></div></div></body></html>
6 changes: 5 additions & 1 deletion doc/html/read-dwarf/Analyse/Collected/index.html
Original file line number Diff line number Diff line change
@@ -1,2 +1,6 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Collected (read-dwarf.Analyse.Collected)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">read-dwarf</a> &#x00BB; <a href="../index.html">Analyse</a> &#x00BB; Collected</nav><h1>Module <code>Analyse.Collected</code></h1><p>collect the various test analysis data</p></header><dl><dt class="spec value" id="val-mk_analysis"><a href="#val-mk_analysis" class="anchor"></a><code><span class="keyword">val</span> mk_analysis : <a href="../ElfTypes/index.html#type-test">ElfTypes.test</a> <span>&#45;&gt;</span> string <span>&#45;&gt;</span> <span>string option</span> <span>&#45;&gt;</span> <a href="../../Analyse__/CollectedType/index.html#type-analysis">Analyse__.CollectedType.analysis</a></code></dt></dl></div></body></html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Collected (read-dwarf.Analyse.Collected)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 3.0.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">Index</a> &#x00BB; <a href="../../index.html">read-dwarf</a> &#x00BB; <a href="../index.html">Analyse</a> &#x00BB; Collected</nav><header class="odoc-preamble"><h1>Module <code><span>Analyse.Collected</span></code></h1><p>collect the various test analysis data</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-mk_analysis"><a href="#val-mk_analysis" class="anchor"></a><code><span><span class="keyword">val</span> mk_analysis :
<span><a href="../ElfTypes/index.html#type-test">ElfTypes.test</a> <span class="arrow">&#45;&gt;</span></span>
<span>string <span class="arrow">&#45;&gt;</span></span>
<span><span>string option</span> <span class="arrow">&#45;&gt;</span></span>
<span class="xref-unresolved">Analyse__.CollectedType.analysis</span></span></code></div></div></div></body></html>
Loading