From 1cc4b8894d348a0fb420cf38040b047dca0ecc7b Mon Sep 17 00:00:00 2001 From: Michael McLoughlin Date: Thu, 7 Mar 2024 15:04:03 -0500 Subject: [PATCH 1/4] asli :ast command for dumping semantics AST --- bin/asli.ml | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/bin/asli.ml b/bin/asli.ml index 75bbd807..c82bea4c 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -40,6 +40,7 @@ let help_msg = [ {|:elf Load an ELF file|}; {|:opcode Decode and execute opcode|}; {|:sem Decode and print opcode semantics|}; + {|:ast Decode and write opcode semantics to a file, in a structured ast format|}; {|:project Execute ASLi commands in |}; {|:q :quit Exit the interpreter|}; {|:run Execute instructions|}; @@ -195,11 +196,17 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 let op = Z.of_string opcode in Printf.printf "Decoding instruction %s %s\n" iset (Z.format "%x" op); cpu'.sem iset op + | [":ast"; iset; opcode] -> + let op = Value.VBits (Primops.prim_cvt_int_bits (Z.of_int 32) (Z.of_string opcode)) in + let decoder = Eval.Env.getDecoder cpu.env (Ident iset) in + List.iter + (fun s -> Printf.printf "%s\n" (Utils.to_string (PP.pp_raw_stmt s))) + (Dis.dis_decode_entry cpu.env cpu.denv decoder op); | ":dump" :: iset :: opcode :: rest -> - let fname = - (match rest with + let fname = + (match rest with | [] -> "sem.aslb" - | [x] -> x + | [x] -> x | _ -> invalid_arg "expected at most 3 arguments to :dump") in let cpu' = Cpu.mkCPU (Eval.Env.copy cpu.env) cpu.denv in @@ -320,15 +327,15 @@ let _ = let main () = if !opt_print_version then Printf.printf "%s\n" version - else if !opt_print_aarch64_dir then - match aarch64_asl_dir with + else if !opt_print_aarch64_dir then + match aarch64_asl_dir with | Some d -> Printf.printf "%s\n" d | None -> (Printf.eprintf "Unable to retrieve installed asl directory\n"; exit 1) else begin if !opt_verbose then List.iter print_endline banner; if !opt_verbose then print_endline "\nType :? for help"; let env_opt = - if (!opt_no_default_aarch64) + if (!opt_no_default_aarch64) then evaluation_environment !opt_prelude !opt_filenames !opt_verbose else begin if List.length (!opt_filenames) != 0 then @@ -338,7 +345,7 @@ let main () = else (); aarch64_evaluation_environment ~verbose:!opt_verbose (); end in - let env = (match env_opt with + let env = (match env_opt with | Some e -> e | None -> failwith "Unable to build evaluation environment.") in if not !opt_no_default_aarch64 then @@ -348,7 +355,7 @@ let main () = LNoise.history_load ~filename:"asl_history" |> ignore; LNoise.history_set ~max_length:100 |> ignore; - + let denv = Dis.build_env env in let prj_files = List.filter (fun f -> Utils.endswith f ".prj") !opt_filenames in let tcenv = TC.Env.mkEnv TC.env0 and cpu = Cpu.mkCPU env denv in From d6948ef8a188b12eace6f898dfa9315ea1e4f2a6 Mon Sep 17 00:00:00 2001 From: Michael McLoughlin Date: Thu, 7 Mar 2024 16:54:40 -0500 Subject: [PATCH 2/4] print optional_else like indented_block --- libASL/asl.ott | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/libASL/asl.ott b/libASL/asl.ott index 77984705..79a6341d 100644 --- a/libASL/asl.ott +++ b/libASL/asl.ott @@ -630,8 +630,12 @@ s_elsif :: 'S_Elsif_' ::= optional_else :: 'S_Else' ::= {{ phantom }} {{ ocaml stmt list }} - {{ pp-raw x = match x with [] -> string "" - | ys -> string "(else " ^^ separate (string "\n") (List.map pp_raw_stmt ys) ^^ string ")" }} + {{ pp-raw x = (nest 4 (lbracket + ^^ hardline + ^^ (separate hardline (List.map pp_raw_stmt x)))) + ^^ hardline + ^^ rbracket + }} {{ pp x = match x with [] -> string "" | ys -> string "else {" ^^ hardline ^^ (nest 4 (separate (string "\n") (List.map pp_stmt ys @ [string "}"]))) From d9138842940b39c1a355f056ffca47102b9cd227 Mon Sep 17 00:00:00 2001 From: Michael McLoughlin Date: Thu, 7 Mar 2024 17:16:25 -0500 Subject: [PATCH 3/4] print blocks with braces --- libASL/asl.ott | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/libASL/asl.ott b/libASL/asl.ott index 79a6341d..b8c36cdc 100644 --- a/libASL/asl.ott +++ b/libASL/asl.ott @@ -516,11 +516,11 @@ stmts :: 'Stmts_' ::= indented_block :: 'Block_' ::= {{ phantom }} {{ ocaml stmt list }} - {{ pp-raw x = (nest 4 (lbracket + {{ pp-raw x = (nest 4 (lbrace ^^ hardline ^^ (separate hardline (List.map pp_raw_stmt x)))) ^^ hardline - ^^ rbracket + ^^ rbrace }} {{ pp x = (nest 4 (lbrace ^^ hardline @@ -630,11 +630,11 @@ s_elsif :: 'S_Elsif_' ::= optional_else :: 'S_Else' ::= {{ phantom }} {{ ocaml stmt list }} - {{ pp-raw x = (nest 4 (lbracket + {{ pp-raw x = (nest 4 (lbrace ^^ hardline ^^ (separate hardline (List.map pp_raw_stmt x)))) ^^ hardline - ^^ rbracket + ^^ rbrace }} {{ pp x = match x with [] -> string "" | ys -> string "else {" ^^ hardline From 2b1ce61d5838fb2800cfef4c3caee563e490cd43 Mon Sep 17 00:00:00 2001 From: Michael McLoughlin Date: Fri, 8 Mar 2024 14:32:56 -0500 Subject: [PATCH 4/4] call pp_raw_indented_block from optional_else --- libASL/asl.ott | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/libASL/asl.ott b/libASL/asl.ott index b8c36cdc..763d3e0c 100644 --- a/libASL/asl.ott +++ b/libASL/asl.ott @@ -630,12 +630,7 @@ s_elsif :: 'S_Elsif_' ::= optional_else :: 'S_Else' ::= {{ phantom }} {{ ocaml stmt list }} - {{ pp-raw x = (nest 4 (lbrace - ^^ hardline - ^^ (separate hardline (List.map pp_raw_stmt x)))) - ^^ hardline - ^^ rbrace - }} + {{ pp-raw x = pp_raw_indented_block x }} {{ pp x = match x with [] -> string "" | ys -> string "else {" ^^ hardline ^^ (nest 4 (separate (string "\n") (List.map pp_stmt ys @ [string "}"])))