Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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
12 changes: 11 additions & 1 deletion cli/lib/isla/converter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,17 @@ let to_assembly_input (ir : Ir.t) : Assembler.assembly_input =
)
ir.symbolic
in
{sections = code_sections; symbols = data_symbols}
let fixed_sections =
List.map
(fun (sec : Ir.section) ->
{ Assembler.name = sec.sec_name;
code = sec.code;
fixed_addr = Some sec.address
}
)
ir.sections
in
{sections = code_sections @ fixed_sections; symbols = data_symbols}

(* {1 Step 4: assembly_result -> Testrepr.t (memory, registers, termination)} *)

Expand Down
33 changes: 33 additions & 0 deletions cli/lib/isla/ir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,12 @@ type thread =
init : (string * value) list
}

type section =
{ sec_name : string;
address : int;
code : string
}

type expect =
| Sat
| Unsat
Expand All @@ -59,6 +65,7 @@ type t =
{ arch : Litmus.Arch_id.t;
name : string;
threads : thread list;
sections : section list;
symbolic : string list;
locations : (string * value) list;
expect : expect;
Expand Down Expand Up @@ -95,6 +102,31 @@ let parse_threads toml =
let table = Otoml.get_table toml in
List.sort (fun a b -> compare a.tid b.tid) (List.map parse_thread table)

let parse_address = function
| Otoml.TomlInteger i -> i
| Otoml.TomlString s -> (
try Z.to_int (Z.of_string s)
with Invalid_argument _ | Z.Overflow ->
raise (Otoml.Type_error ("invalid address: " ^ s))
)
| v ->
raise
(Otoml.Type_error
("address must be integer or hex string, got: "
^ Otoml.Printer.to_string v
)
)

let parse_section (name, table) =
let _ = Otoml.get_table table in
let address = Otoml.find table parse_address ["address"] in
let code = Otoml.find table Otoml.get_string ["code"] |> String.trim in
{sec_name = name; address; code}

let parse_sections toml =
let table = Otoml.get_table toml in
List.map parse_section table

let parse_expect toml =
match Otoml.get_string toml with
| "sat" -> Sat
Expand Down Expand Up @@ -122,6 +154,7 @@ let of_toml toml =
{ arch = Otoml.find toml parse_arch ["arch"];
name = Otoml.find_or ~default:"unknown" toml Otoml.get_string ["name"];
threads = Otoml.find toml parse_threads ["thread"];
sections = Otoml.find_or ~default:[] toml parse_sections ["section"];
symbolic =
Otoml.find_or ~default:[] toml
(Otoml.get_array Otoml.get_string)
Expand Down
Loading