Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
90 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
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/analyse/CallGraph.ml
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ type call_graph_node = addr * index * string list
let mk_call_graph test (an : CollectedType.analysis) =
let mask_addr x:natural =
if !Globals.morello
then Nat_big_num.shift_left (Nat_big_num.shift_right x 1) 1
then Sym.shift_left (Sym.shift_right x 1) 1
else x in
(* take the nodes to be all the elf symbol addresses of stt_func
symbol type (each with their list of elf symbol names) together
Expand Down Expand Up @@ -110,7 +110,7 @@ let mk_call_graph test (an : CollectedType.analysis) =
if
not
(List.exists
(function (a'', _) -> Nat_big_num.equal a' a'')
(function (a'', _) -> Sym.Ordered.equal a' a'')
elf_symbols)
then Some (a', ["FROM BL:" ^ s'])
else None)
Expand All @@ -122,7 +122,7 @@ let mk_call_graph test (an : CollectedType.analysis) =
match axs with
| [] -> acc
| (a, x) :: axs' ->
if not (List.exists (function (a', _) -> Nat_big_num.equal a a') acc) then
if not (List.exists (function (a', _) -> Sym.Ordered.equal a a') acc) then
dedup axs' ((a, x) :: acc)
else dedup axs' acc
in
Expand All @@ -133,7 +133,7 @@ let mk_call_graph test (an : CollectedType.analysis) =
List.sort
(function
| (a, _) -> (
function (a', _) -> Nat_big_num.compare a a'
function (a', _) -> Sym.Ordered.compare a a'
))
(elf_symbols @ extra_bl_targets)
in
Expand Down
214 changes: 143 additions & 71 deletions src/analyse/ControlFlow.ml

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion src/analyse/ControlFlowPpDot.ml
Original file line number Diff line number Diff line change
Expand Up @@ -793,7 +793,7 @@ let mk_cfg test an visitedo node_name_prefix (recurse_flat : bool) (_inline_all
let ((_comp_dir, _dir, _file) as ufe) =
Dwarf.unpack_file_entry lnh lnr.lnr_file
in
(ufe, Nat_big_num.to_int lnr.lnr_line))
(ufe, Sym.to_int lnr.lnr_line))
an.line_info.(k))
in

Expand Down
1 change: 1 addition & 0 deletions src/analyse/ControlFlowTypes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,7 @@ type instruction = {
i_operands : string;
i_control_flow : control_flow_insn;
i_targets : target list;
i_relocation : (string * string) option;
}

type come_from = {
Expand Down
7 changes: 4 additions & 3 deletions src/analyse/DwarfFrameInfo.ml
Original file line number Diff line number Diff line change
Expand Up @@ -53,14 +53,15 @@ open ControlFlowTypes

let aof ((a : natural), (_cfa : string), (_regs : (string * string) list)) = a

(* TODO does Sym.Ordered work as we want? *)
let rec f (aof : 'b -> natural) (a : natural) (last : 'b option) (bs : 'b list) : 'b option =
match (last, bs) with
| (None, []) -> None
| (Some b', []) -> if Nat_big_num.greater_equal a (aof b') then Some b' else None
| (Some b', []) -> if Sym.Ordered.greater_equal a (aof b') then Some b' else None
| (None, b'' :: bs') -> f aof a (Some b'') bs'
| (Some b', b'' :: bs') ->
if Nat_big_num.less a (aof b') then None
else if Nat_big_num.greater_equal a (aof b') && Nat_big_num.less a (aof b'') then Some b'
if Sym.Ordered.less a (aof b') then None
else if Sym.Ordered.greater_equal a (aof b') && Sym.Ordered.less a (aof b'') then Some b'
else f aof a (Some b'') bs'

let mk_frame_info test instructions :
Expand Down
6 changes: 3 additions & 3 deletions src/analyse/DwarfInliningInfo.ml
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ let mk_inlining test sdt instructions =
let addr = i.i_addr in
let issr_still_current =
List.filter
(function (_label, ((_n1, n2), (_m, _n), _is)) -> Nat_big_num.less addr n2)
(function (_label, ((_n1, n2), (_m, _n), _is)) -> Sym.Ordered.less addr n2)
issr_current
in

Expand All @@ -83,8 +83,8 @@ let mk_inlining test sdt instructions =

let (issr_starting_here0, issr_rest') =
find_first
(function ((_n1, n2), (_m, _n), _is) -> Nat_big_num.less_equal n2 addr)
(function ((n1, _n2), (_m, _n), _is) -> Nat_big_num.equal n1 addr)
(function ((_n1, n2), (_m, _n), _is) -> Sym.Ordered.less_equal n2 addr)
(function ((n1, _n2), (_m, _n), _is) -> Sym.Ordered.equal n1 addr)
[] issr_rest
in

Expand Down
65 changes: 33 additions & 32 deletions src/analyse/DwarfLineInfo.ml
Original file line number Diff line number Diff line change
Expand Up @@ -86,18 +86,18 @@ type evaluated_line_info_for_instruction = {
(* line number sequences can overlap, and we have to walk through instructions (not addresses), so we simplify by splitting all of them into individual entries, sort them by first address, and then walk through them painting a per-instruction array. This is algorithmically a bit terrible, but seems to add only a couple of seconds to read-dwarf rd *)

let pp_line_number_header_concise (lnh : Dwarf.line_number_header) : string =
"lnh offset = " ^ Dwarf.pphex lnh.lnh_offset ^ "\n"
"lnh offset = " ^ Dwarf.pphex_sym lnh.lnh_offset ^ "\n"

(*^ ("dwarf_format = " ^ (pp_dwarf_format lnh.lnh_dwarf_format ^ ("\n"
^ ("unit_length = " ^ (Nat_big_num.to_string lnh.lnh_unit_length ^ ("\n"
^ ("version = " ^ (Nat_big_num.to_string lnh.lnh_version ^ ("\n"
^ ("header_length = " ^ (Nat_big_num.to_string lnh.lnh_header_length ^ ("\n"
^ ("minimum_instruction_length = " ^ (Nat_big_num.to_string lnh.lnh_minimum_instruction_length ^ ("\n"
^ ("maximum_operations_per_instruction = " ^ (Nat_big_num.to_string lnh.lnh_maximum_operations_per_instruction ^ ("\n"
^ ("unit_length = " ^ (Sym.to_string lnh.lnh_unit_length ^ ("\n"
^ ("version = " ^ (Sym.to_string lnh.lnh_version ^ ("\n"
^ ("header_length = " ^ (Sym.to_string lnh.lnh_header_length ^ ("\n"
^ ("minimum_instruction_length = " ^ (Sym.to_string lnh.lnh_minimum_instruction_length ^ ("\n"
^ ("maximum_operations_per_instruction = " ^ (Sym.to_string lnh.lnh_maximum_operations_per_instruction ^ ("\n"
^ ("default_is_stmt = " ^ (string_of_bool lnh.lnh_default_is_stmt ^ ("\n"
^ ("line_base = " ^ (Nat_big_num.to_string lnh.lnh_line_base ^ ("\n"
^ ("line_range = " ^ (Nat_big_num.to_string lnh.lnh_line_range ^ ("\n"
^ ("opcode_base = " ^ (Nat_big_num.to_string lnh.lnh_opcode_base ^ ("\n"
^ ("line_base = " ^ (Sym.to_string lnh.lnh_line_base ^ ("\n"
^ ("line_range = " ^ (Sym.to_string lnh.lnh_line_range ^ ("\n"
^ ("opcode_base = " ^ (Sym.to_string lnh.lnh_opcode_base ^ ("\n"
^ ("standard_opcode_lengths = " ^ (string_of_list
instance_Show_Show_Num_natural_dict lnh.lnh_standard_opcode_lengths ^ ("\n"
^ ("comp_dir = " ^ (string_of_maybe
Expand Down Expand Up @@ -136,7 +136,8 @@ let split_into_sequences
| None -> fatal "split_into_sequences found sequence of length 0"
in
let last = lnr.lnr_address in
if Nat_big_num.equal first last then fatal "split_into_sequences found first=last"
(* print_endline (Dwarf.pphex_sym first ^ " " ^ Dwarf.pphex_sym last); *)
if Sym.equal first last then fatal "split_into_sequences found first=last"
else ();
let elis =
{
Expand All @@ -160,8 +161,8 @@ let split_into_entries (s : evaluated_line_info_sequence) : evaluated_line_info_
{
elie_first = l1.lnr_address;
elie_last =
( if Nat_big_num.equal l2.lnr_address l1.lnr_address then l1.lnr_address
else Nat_big_num.sub l2.lnr_address (Nat_big_num.of_int 1)
( if Sym.equal l2.lnr_address l1.lnr_address then l1.lnr_address
else Sym.sub l2.lnr_address (Sym.of_int 1)
);
elie_lnh = s.elis_lnh;
elie_lnr = l1;
Expand All @@ -176,9 +177,9 @@ let split_into_entries (s : evaluated_line_info_sequence) : evaluated_line_info_

let mk_line_info (eli: Dwarf.evaluated_line_info) instructions : evaluated_line_info_for_instruction option array =
let sequences = List.flatten (List.map split_into_sequences eli) in
let compare_sequence s1 s2 = Nat_big_num.compare s1.elis_first s2.elis_first in
let compare_sequence s1 s2 = Sym.compare s1.elis_first s2.elis_first in
let sequences_sorted = List.sort compare_sequence sequences in
(*let overlap_sequence s1 s2 = not( Nat_big_num.greater_equal s2.first s1.last || Nat_big_num.greater_equal s1.first s2.last) in*)
(*let overlap_sequence s1 s2 = not( Sym.greater_equal s2.first s1.last || Sym.greater_equal s1.first s2.last) in*)

Printf.printf "mk_line_info\n%s" (String.concat "\n" (List.map pp_sequence_concise sequences_sorted));

Expand All @@ -189,12 +190,12 @@ let mk_line_info (eli: Dwarf.evaluated_line_info) instructions : evaluated_line_
let (discardable,remaining') =
List.partition
(function sequence ->
Nat_big_num.less_equal sequence.elis_last addr)
Sym.less_equal sequence.elis_last addr)
remaining_sequences in
let (sequences,remaining'') =
List.partition
(function sequence ->
Nat_big_num.less_equal sequence.elis_first addr)
Sym.less_equal sequence.elis_first addr)
remaining' in
(sequences,remaining'') in

Expand Down Expand Up @@ -224,23 +225,23 @@ let mk_line_info (eli: Dwarf.evaluated_line_info) instructions : evaluated_line_
let addr = instructions.(k).i_addr in
match remaining_lines with
| l1::((l2::remaining_lines') as remaining_lines'') ->
if Nat_big_num.equal addr l1.lnr_address then
if Sym.equal addr l1.lnr_address then
(* this instruction address exactly matches the first line of this sequence *)
let elifi = {
elifi_start = true;
elifi_lnh = active_sequence.elis_lnh;
elifi_line = l1 } in
elifis.(k) <- Some elifi;
f active_sequence remaining_lines remaining_sequences (k+1)
else if Nat_big_num.less l1.lnr_address addr && Nat_big_num.less addr l2.lnr_address then
else if Sym.less l1.lnr_address addr && Sym.less addr l2.lnr_address then
(* this instruction address is within the range of the first line, but not equal to it*)
let elifi = {
elifi_start = false;
elifi_lnh = active_sequence.elis_lnh;
elifi_line = l1 } in
elifis.(k) <- Some elifi;
f active_sequence remaining_lines remaining_sequences (k+1)
else if Nat_big_num.greater_equal addr l2.lnr_address then
else if Sym.greater_equal addr l2.lnr_address then
(* this instruction address is after the range of the first line *)
if not(l2.lnr_end_sequence (* invariant: iff remaining'=[]*)) then
(* there are more non-end lines left in this sequence: try again with the next *)
Expand Down Expand Up @@ -268,11 +269,11 @@ let mk_line_info (eli : Dwarf.evaluated_line_info) instructions :
let elifis = Array.make size [] in

let sequences = List.flatten (List.map split_into_sequences eli) in
let compare_sequence s1 s2 = Nat_big_num.compare s1.elis_first s2.elis_first in
let compare_sequence s1 s2 = Sym.Ordered.compare s1.elis_first s2.elis_first in
let sequences_sorted = List.sort compare_sequence sequences in

let entries = List.flatten (List.map split_into_entries sequences_sorted) in
let compare_entry e1 e2 = Nat_big_num.compare e1.elie_first e2.elie_first in
let compare_entry e1 e2 = Sym.Ordered.compare e1.elie_first e2.elie_first in
let entries_sorted = List.sort compare_entry entries in

(*List.iter (function elie -> Printf.printf "%s" (pp_elie_concise elie)) entries_sorted;*)
Expand All @@ -285,15 +286,15 @@ let mk_line_info (eli : Dwarf.evaluated_line_info) instructions :
match remaining with
| [] -> (acc, remaining)
| elie :: remaining' ->
if Nat_big_num.less_equal elie.elie_first addr then
if Sym.Ordered.less_equal elie.elie_first addr then
mk_new_perhaps_relevant (elie :: acc) remaining'
else (acc, remaining)
in

let (new_perhaps_relevant, remaining') = mk_new_perhaps_relevant [] remaining_entries in

let addr_in elie =
Nat_big_num.less_equal elie.elie_first addr && Nat_big_num.less_equal addr elie.elie_last
Sym.in_range elie.elie_first elie.elie_last addr
in

let still_active_entries =
Expand All @@ -305,7 +306,7 @@ let mk_line_info (eli : Dwarf.evaluated_line_info) instructions :
(function
| elie ->
let elifi =
{ elifi_start = Nat_big_num.equal addr elie.elie_first; elifi_entry = elie }
{ elifi_start = Sym.equal addr elie.elie_first; elifi_entry = elie }
in
elifi)
still_active_entries;
Expand Down Expand Up @@ -443,14 +444,14 @@ let pp_dwarf_source_file_lines' m (ds : Dwarf.dwarf_static) (pp_actual_line : bo
| Ascii -> s
| Html ->
"@<a class=\"link-inst\" href=\"" ^ "" ^ file ^ ".html#"
^ Nat_big_num.to_string lnr.lnr_line
^ Sym.to_string lnr.lnr_line
^ "\">" ^ s ^ "</a>@ "
in
wrap_link m
(subprogram_name ^ ":"
^ Nat_big_num.to_string lnr.lnr_line
^ Sym.to_string lnr.lnr_line
^ "."
^ Nat_big_num.to_string lnr.lnr_column
^ Sym.to_string lnr.lnr_column
^ " (" ^ file ^ ")"
)
(* ^ (if elifi.elifi_start then "S" else "s")*)
Expand All @@ -463,10 +464,10 @@ let pp_dwarf_source_file_lines' m (ds : Dwarf.dwarf_static) (pp_actual_line : bo
^ " "
^
if pp_actual_line then
let line = Nat_big_num.to_int lnr.lnr_line in
let line = Sym.to_int lnr.lnr_line in
if line = 0 then "line 0"
else
pp_source_line (source_line (comp_dir, dir, file) line) (Nat_big_num.to_int lnr.lnr_column)
pp_source_line (source_line (comp_dir, dir, file) line) (Sym.to_int lnr.lnr_column)
else ""

(* OLD source line number for O0/2 correlation
Expand All @@ -479,11 +480,11 @@ let rec dwarf_source_file_line_numbers' test recursion_limit (a : natural) :
match sls with
| [] ->
dwarf_source_file_line_numbers' test (recursion_limit - 1)
(Nat_big_num.sub a (Nat_big_num.of_int 4))
(Sym.sub a (Sym.of_int 4))
| _ ->
List.map
(fun ((comp_dir, dir, file), n, lnr, subprogram_name) ->
(subprogram_name, Nat_big_num.to_int n))
(subprogram_name, Sym.to_int n))
sls

let dwarf_source_file_line_numbers test (a : natural) =
Expand All @@ -507,7 +508,7 @@ let dwarf_source_file_line_numbers_by_index test line_info k :
Dwarf.subprogram_at_line test.dwarf_static.ds_subprogram_line_extents ufe
lnr.lnr_line )
in
(subprogram_name, Nat_big_num.to_int lnr.lnr_line))
(subprogram_name, Sym.to_int lnr.lnr_line))
elifis)
in
match lines with [_] -> lines | [] -> lines | _ -> []
Loading