Added json export for the abstract ARM Assembler

The json export for the abstract ARM Assembler is quite similar
to it's PowerPC equivalent expect for the different instruction
arguments.
Bug 22472

1 files changed, 273 insertions, 3 deletions

diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index 74c64180..45433064 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -3,6 +3,7 @@
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
 (*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*          Michael Schmidt, AbsInt Angewandte Informatik GmbH         *)
 (*                                                                     *)
 (*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
 (*  is distributed under the terms of the INRIA Non-Commercial         *)
@@ -12,9 +13,278 @@
 
 (* Simple functions to serialize arm Asm to JSON *)
 
-(* Dummy function *)
+open Asm
+open AST
+open BinNums
+open Camlcoq
+open Json
+
+let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "Pbc"; "Pbic"; "Pblreg";
+                       "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pfcpy_iif";
+                       "Pfcpy_fii"; "Pfcpy_fi"; "Pfcpy_sf"; "Pdmb"; "Pdsb"; "Peor"; "Pfabsd";
+                       "Pfabss"; "Pfaddd"; "Pfadds"; "Pfcmpd"; "Pfcmps"; "Pfcmpzd"; "Pfcmpzs";
+                       "Pfcpyd"; "Pfcpy_fs"; "Pfcpy_if";"Pfcvtds"; "Pfcvtsd"; "Pfdivd"; "Pfdivs"; "Pfldd";
+                       "Pfldd_a"; "Pflds"; "Pflid"; "Pflis"; "Pfmuld"; "Pfmuls"; "Pfnegd";
+                       "Pfnegs"; "Pfreeframe"; "Pfsitod"; "Pfsitos"; "Pfsqrt"; "Pfstd"; "Pfstd_a";
+                       "Pfsts"; "Pfsubd"; "Pfsubs"; "Pftosizd"; "Pftosizs"; "Pftouizd";
+                       "Pftouizs"; "Pfuitod"; "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr";
+                       "Pldr_a"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb";
+                       "Pldrsh"; "Ploadsymbol"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite";
+                       "Pmovt"; "Pmovw"; "Pmul"; "Pmvn"; "Porr"; "Ppush"; "Prev"; "Prev16"; "Prsb";
+                       "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull"; "Pstr"; "Pstr_a";
+                       "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv";
+                       "Pumull" ]
+
+type instruction_arg =
+  | ALabel of positive
+  | Atom of positive
+  | DFreg of freg
+  | Float32 of Floats.float32
+  | Float64 of Floats.float
+  | Id
+  | Ireg of ireg
+  | Long of Integers.Int.int
+  | SFreg of freg
+  | SPreg of sreg
+  | Shift of shift_op
+  | String of string
+  | Symbol of ident * BinNums.coq_Z
+  | Condition of string
+
+let pp_reg pp reg =
+  pp_jsingle_object pp "Register" pp_jstring reg
+
+let pp_ireg pp reg =
+  pp_reg pp (TargetPrinter.int_reg_name reg)
+
+let pp_freg pp reg =
+  pp_reg pp (TargetPrinter.float_reg_name reg)
+
+let pp_single_freg pp reg =
+  pp_reg pp (TargetPrinter.single_float_reg_name reg)
+
+let pp_single_param_reg pp reg =
+  pp_reg pp (TargetPrinter.single_param_reg_name reg)
+
+let pp_shiftreg pp (r, op, n) =
+  pp_jobject_start pp;
+  pp_jmember ~first:true pp "Register" pp_ireg r;
+  pp_jmember pp "Op" pp_jstring op;
+  pp_jmember pp "Amount" pp_z n;
+  pp_jobject_end pp
+
+let pp_shiftop pp so =
+  let (r, op, n) = match so with
+    | SOimm n     -> (None, None, Some n)
+    | SOreg r     -> (Some r, None, None)
+    | SOlsl(r, n) -> (Some r, Some "lsl", Some n)
+    | SOlsr(r, n) -> (Some r, Some "lsr", Some n)
+    | SOasr(r, n) -> (Some r, Some "asr", Some n)
+    | SOror(r, n) -> (Some r, Some "ror", Some n)
+  in
+  match (r, op, n) with
+    | (None, None, Some n)      -> pp_jsingle_object pp "Integer" pp_int64 n
+    | (Some r, None, None)      -> pp_ireg pp r
+    | (Some r, Some op, Some n) -> pp_jsingle_object pp "ShiftedRegister" pp_shiftreg (r, op, n)
+    | _ -> assert false
+
+let pp_testcond pp bit =
+  pp_jsingle_object pp "Condition" pp_jstring bit
+
+let pp_label pp l =
+  pp_jsingle_object pp "Label" pp_jint32 (P.to_int32 l)
+
+let pp_symbol pp (id, ofs) =
+  pp_jobject_start pp;
+  pp_jmember ~first:true pp "Name" pp_atom id;
+  pp_jmember pp "Offset" pp_z ofs;
+  pp_jobject_end pp
+
+
+let pp_arg pp = function
+  | ALabel lbl -> pp_label pp lbl
+  | Atom a -> pp_atom_constant pp a
+  | DFreg fr -> pp_freg pp fr
+  | Float32 f -> pp_float32_constant pp f
+  | Float64 f  -> pp_float64_constant pp f
+  | Id ->  pp_id_const pp ()
+  | Ireg ir -> pp_ireg pp ir
+  | Long i ->  pp_jsingle_object pp "Integer" pp_int64 i
+  | SFreg fr -> pp_single_freg pp fr
+  | SPreg sr -> pp_single_param_reg pp sr
+  | Shift so -> pp_shiftop pp so
+  | String s -> pp_jsingle_object pp "String" pp_jstring s
+  | Symbol (id, ofs) -> pp_jsingle_object pp "Symbol" pp_symbol (id, ofs)
+  | Condition b -> pp_testcond pp b
+
+
+let pp_instructions pp ic =
+  let ic = List.filter (fun s -> match s with
+      | Pbuiltin (ef,_,_) ->
+        begin match ef with
+          | EF_inline_asm _
+          | EF_annot _ -> true
+          | _ -> false
+        end
+      (* Only debug relevant *)
+      | Pcfi_adjust _
+      | Pcfi_rel_offset _ -> false
+      | _ -> true) ic in
+
+  let instruction pp n args =
+    assert (List.mem n mnemonic_names);
+    pp_jobject_start pp;
+    pp_jmember ~first:true pp "Instruction Name" pp_jstring n;
+    pp_jmember pp "Args" (pp_jarray pp_arg) args;
+    pp_jobject_end pp
+  in
+
+  let [@ocaml.warning "+4"] instruction pp = function
+    | Pbuiltin (ef, args, _) ->
+      begin match ef with
+        | EF_inline_asm _ ->
+          instruction pp "Pinlineasm" [Id];
+          Cerrors.warning ("", -10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump"
+        | EF_annot (kind,txt, targs) ->
+          let annot_string = PrintAsmaux.annot_text TargetPrinter.preg_annot "r1" (camlstring_of_coqstring txt) args in
+          let len = String.length annot_string in
+          let buf = Buffer.create len in
+          String.iter (fun c -> begin match c with
+              | '\\' | '"' -> Buffer.add_char buf '\\'
+              | _ -> () end;
+              Buffer.add_char buf c) annot_string;
+          let annot_string = Buffer.contents buf in
+        let kind = match P.to_int kind with
+          | 1 -> "normal"
+          | 2 -> "ais"
+          | _ -> assert false in
+          instruction pp "Pannot" [String kind;String annot_string]
+        (* Builtins that are not exported to JSON *)
+        | EF_annot_val _
+        | EF_builtin _
+        | EF_debug _
+        | EF_external _
+        | EF_free
+        | EF_malloc
+        | EF_memcpy _
+        | EF_runtime _
+        | EF_vload _
+        | EF_vstore _ -> assert false
+      end
+    (* Stackframe, should not occur *)
+    | Pallocframe _ -> assert false
+    | Pfreeframe _  -> assert false
+    (* Call Frame Information, only debug relevant and not exported *)
+    | Pcfi_adjust _ -> assert false
+    | Pcfi_rel_offset _ -> assert false
+    (* ARM instructions *)
+    | Padc(r1, r2, so) -> instruction pp "Padc" [Ireg r1; Ireg r2; Shift so]
+    | Padd(r1, r2, so) -> instruction pp "Padd" [Ireg r1; Ireg r2; Shift so]
+    | Padds(r1, r2, so) -> instruction pp "Padds" [Ireg r1; Ireg r2; Shift so]
+    | Pand(r1, r2, so) -> instruction pp "Pand" [Ireg r1; Ireg r2; Shift so]
+    | Pasr(r1, r2, r3) -> instruction pp "Pasr" [Ireg r1; Ireg r2; Ireg r3]
+    | Pb(lbl) -> instruction pp "Pb" [ALabel lbl]
+    | Pbc(bit, lbl) -> instruction pp "Pbc" [Condition (TargetPrinter.condition_name bit); ALabel lbl]
+    | Pbic(r1, r2, so) -> instruction pp "Pbic" [Ireg r1; Ireg r2; Shift so]
+    | Pblreg(r, sg) -> instruction pp "Pblreg" [Ireg r]
+    | Pblsymb(id, sg) -> instruction pp "Pblsymb" [Atom id]
+    | Pbne(lbl) -> instruction pp "Pbne" [ALabel lbl]
+    | Pbreg(r, sg) -> instruction pp "Pbreg" [Ireg r]
+    | Pbsymb(id, sg) -> instruction pp "Pbsymb" [Atom id]
+    | Pbtbl(r, tbl) -> instruction pp "Pbtbl" ((Ireg r)::(List.map (fun a -> ALabel a) tbl))
+    | Pclz(r1, r2) -> instruction pp "Pclz" [Ireg r1; Ireg r2]
+    | Pcmp(r1,so) -> instruction pp "Pcmp" [Ireg r1; Shift so]
+    | Pdmb -> instruction pp "Pdmb" []
+    | Pdsb -> instruction pp "Pdsb" []
+    | Peor(r1, r2, so) -> instruction pp "Peor" [Ireg r1; Ireg r2; Shift so]
+    | Pfabsd(r1, r2) -> instruction pp "Pfabsd" [DFreg r1; DFreg r2]
+    | Pfabss(r1, r2) -> instruction pp "Pfabss" [SFreg r1; SFreg r2]
+    | Pfaddd(r1, r2, r3) -> instruction pp "Pfaddd" [DFreg r1; DFreg r2; DFreg r3]
+    | Pfadds(r1, r2, r3) -> instruction pp "Pfadds" [SFreg r1; SFreg r2; SFreg r3]
+    | Pfcmpd(r1, r2) -> instruction pp "Pfcmpd" [DFreg r1; DFreg r2]
+    | Pfcmps(r1, r2) -> instruction pp "Pfcmps" [SFreg r1; SFreg r2]
+    | Pfcmpzd(r1) -> instruction pp "Pfcmpzd" [DFreg r1]
+    | Pfcmpzs(r1) -> instruction pp "Pfcmpzs" [SFreg r1]
+    | Pfcpyd(r1, r2) -> instruction pp "Pfcpyd" [DFreg r1; DFreg r2]
+    | Pfcvtds(r1, r2) -> instruction pp "Pfcvtds" [DFreg r1; SFreg r2]
+    | Pfcvtsd(r1, r2) -> instruction pp "Pfcvtsd" [SFreg r1; DFreg r2]
+    | Pfdivd(r1, r2, r3) -> instruction pp "Pfdivd" [DFreg r1; DFreg r2; DFreg r3]
+    | Pfdivs(r1, r2, r3) -> instruction pp "Pfdivs" [SFreg r1; SFreg r2; SFreg r3]
+    | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) -> instruction pp "Pfldd" [DFreg r1; Ireg r2; Long n]
+    | Pflds(r1, r2, n) -> instruction pp "Pflds" [SFreg r1; Ireg r2; Long n]
+    | Pflid(r1, f) -> instruction pp "Pflid" [DFreg r1; Float64 f]
+    | Pflis(r1, f) -> instruction pp "Pflis" [SFreg r1; Float32 f]
+    | Pfmuld(r1, r2, r3) -> instruction pp "Pfmuld" [DFreg r1; DFreg r2; DFreg r3]
+    | Pfmuls(r1, r2, r3) -> instruction pp "Pfmuls" [SFreg r1; SFreg r2; SFreg r3]
+    | Pfnegd(r1, r2) -> instruction pp "Pfnegd" [DFreg r1; DFreg r2]
+    | Pfnegs(r1, r2) -> instruction pp "Pfnegs" [SFreg r1; SFreg r2]
+    | Pfsitod(r1, r2) -> instruction pp "Pfsitod" [DFreg r1; Ireg r2]
+    | Pfsitos(r1, r2) -> instruction pp "Pfsitos" [SFreg r1; Ireg r2]
+    | Pfsqrt(r1, r2) -> instruction pp "Pfsqrt" [DFreg r1; DFreg r2]
+    | Pfstd(r1, r2, n) | Pfstd_a(r1, r2, n) -> instruction pp "Pfstd" [DFreg r1; Ireg r2; Long n]
+    | Pfsts(r1, r2, n) -> instruction pp "Pfsts" [SFreg r1; Ireg r2; Long n]
+    | Pfsubd(r1, r2, r3) -> instruction pp "Pfsubd" [DFreg r1; DFreg r2; DFreg r3]
+    | Pfsubs(r1, r2, r3) -> instruction pp "Pfsubs" [SFreg r1; SFreg r2; SFreg r3]
+    | Pftosizd(r1, r2) -> instruction pp "Pftosizd" [Ireg r1; DFreg r2]
+    | Pftosizs(r1, r2) -> instruction pp "Pftosizs" [Ireg r1; SFreg r2]
+    | Pftouizd(r1, r2) -> instruction pp "Pftouizd" [Ireg r1; DFreg r2]
+    | Pftouizs(r1, r2) -> instruction pp "Pftouizs" [Ireg r1; SFreg r2]
+    | Pfuitod(r1, r2) -> instruction pp "Pfuitod" [DFreg r1; Ireg r2]
+    | Pfuitos(r1, r2) -> instruction pp "Pfuitos" [SFreg r1; Ireg r2]
+    | Pisb -> instruction pp "Pisb" []
+    | Plabel l -> instruction pp "Plabel" [ALabel l]
+    | Pldr(r1, r2, so) | Pldr_a(r1, r2, so) -> instruction pp "Pldr" [Ireg r1; Ireg r2; Shift so]
+    | Pldr_p(r1, r2, so) -> instruction pp "Pldr_p" [Ireg r1; Ireg r2; Shift so]
+    | Pldrb(r1, r2, so) -> instruction pp "Pldrb" [Ireg r1; Ireg r2; Shift so]
+    | Pldrb_p(r1, r2, so) -> instruction pp "Pldrb_p" [Ireg r1; Ireg r2; Shift so]
+    | Pldrh(r1, r2, so) -> instruction pp "Pldrh" [Ireg r1; Ireg r2; Shift so]
+    | Pldrh_p(r1, r2, so) -> instruction pp "Pldrh_p" [Ireg r1; Ireg r2; Shift so]
+    | Pldrsb(r1, r2, so) -> instruction pp "Pldrsb" [Ireg r1; Ireg r2; Shift so]
+    | Pldrsh(r1, r2, so) -> instruction pp "Pldrsh" [Ireg r1; Ireg r2; Shift so]
+    | Ploadsymbol(r1, id, ofs) -> instruction pp "Ploadsymbol" [Ireg r1; Symbol (id, ofs)]
+    | Plsl(r1, r2, r3) -> instruction pp "Plsl" [Ireg r1; Ireg r2; Ireg r3]
+    | Plsr(r1, r2, r3) -> instruction pp "Plsr" [Ireg r1; Ireg r2; Ireg r3]
+    | Pmla(r1, r2, r3, r4) -> instruction pp "Pmla" [Ireg r1; Ireg r2; Ireg r3; Ireg r4]
+    | Pmov(r1, so) -> instruction pp "Pmov" [Ireg r1; Shift so]
+    | Pmovite(cond, r1, so1, so2) -> instruction pp "Pmovite" [Ireg r1; Condition (TargetPrinter.condition_name cond); Shift so1; Condition (TargetPrinter.neg_condition_name cond); Shift so2]
+    | Pmovt(r1, n) -> instruction pp "Pmovt" [Ireg r1; Long n]
+    | Pmovw(r1, n) -> instruction pp "Pmovw" [Ireg r1; Long n]
+    | Pmul(r1, r2, r3) -> instruction pp "Pmul" [Ireg r1; Ireg r2; Ireg r3]
+    | Pmvn(r1, so) -> instruction pp "Pmvn" [Ireg r1; Shift so]
+    | Porr(r1, r2, so) -> instruction pp "Porr" [Ireg r1; Ireg r2; Shift so]
+    | Ppush(rl) -> instruction pp "Ppush" (List.map (fun r -> Ireg r) rl)
+    | Prev(r1, r2) -> instruction pp "Prev" [Ireg r1; Ireg r2]
+    | Prev16(r1, r2) -> instruction pp "Prev16" [Ireg r1; Ireg r2]
+    | Prsb(r1, r2, so) -> instruction pp "Prsb" [Ireg r1; Ireg r2; Shift so]
+    | Prsbs(r1, r2, so) -> instruction pp "Prsbs" [Ireg r1; Ireg r2; Shift so]
+    | Prsc(r1, r2, so) -> instruction pp "Prsc" [Ireg r1; Ireg r2; Shift so]
+    | Psbc(r1, r2, so) -> instruction pp "Psbc" [Ireg r1; Ireg r2; Shift so]
+    | Psbfx(r1, r2, lsb, sz) -> instruction pp "Psbfx" [Ireg r1; Ireg r2; Long lsb; Long sz]
+    | Psdiv -> instruction pp "Psdiv" [Ireg IR0; Ireg IR1]
+    | Psmull(r1, r2, r3, r4) -> instruction pp "Psmull" [Ireg r1; Ireg r2; Ireg r3; Ireg r4]
+    | Pstr(r1, r2, so) | Pstr_a(r1, r2, so) -> instruction pp "Pstr" [Ireg r1; Ireg r2; Shift so]
+    | Pstr_p(r1, r2, so) -> instruction pp "Pstr_p" [Ireg r1; Ireg r2; Shift so]
+    | Pstrb(r1, r2, so) -> instruction pp "Pstrb" [Ireg r1; Ireg r2; Shift so]
+    | Pstrb_p(r1, r2, so) -> instruction pp "Pstrb_p" [Ireg r1; Ireg r2; Shift so]
+    | Pstrh(r1, r2, so) -> instruction pp "Pstrh" [Ireg r1; Ireg r2; Shift so]
+    | Pstrh_p(r1, r2, so) -> instruction pp "Pstrh_p" [Ireg r1; Ireg r2; Shift so]
+    | Psub(r1, r2, so) -> instruction pp "Psub" [Ireg r1; Ireg r2; Shift so]
+    | Psubs(r1, r2, so) -> instruction pp "Psubs" [Ireg r1; Ireg r2; Shift so]
+    | Pudiv -> instruction pp "Pudiv" [Ireg IR0; Ireg IR1]
+    | Pumull(r1, r2, r3, r4) -> instruction pp "Pumull" [Ireg r1; Ireg r2; Ireg r3; Ireg r4]
+    (* Fixup instructions for calling conventions *)
+    | Pfcpy_fs(r1, r2) -> instruction pp "Pfcpy_fs" [SFreg r1; SPreg r2]
+    | Pfcpy_sf(r1, r2) -> instruction pp "Pfcpy_sf" [SPreg r1; SFreg r2]
+    | Pfcpy_fii(r1, r2, r3) -> instruction pp "Pfcpy_fii" [DFreg r1; Ireg r2; Ireg r3]
+    | Pfcpy_fi(r1, r2) -> instruction pp "Pfcpy_fi" [SFreg r1; Ireg r2]
+    | Pfcpy_iif(r1, r2, r3) -> instruction pp "Pfcpy_iif" [Ireg r1; Ireg r2; DFreg r3]
+    | Pfcpy_if (r1,r2) -> instruction pp "Pfcpy_if" [Ireg r1; SFreg r2]
+  in
+    pp_jarray instruction pp ic
 
 let pp_program pp prog =
-  Format.fprintf pp "null"
+  reset_id ();
+  JsonAST.pp_program pp pp_instructions prog
 
-let pp_mnemonics pp = ()
+let pp_mnemonics pp =
+  JsonAST.pp_mnemonics pp mnemonic_names