1signature arm_evalLib = 2sig 3 type arm_load = patriciaLib.term_ptree * (string, Arbnum.num) Redblackmap.dict 4 5 val arm_load_empty : arm_load 6 7 val arm_load_from_elf : string -> string -> arm_load -> arm_load 8 val arm_load_from_file : string -> string -> arm_load -> arm_load 9 val arm_load_from_string : string -> string -> arm_load -> arm_load 10 val arm_load_from_quote : string -> string frag list -> arm_load -> arm_load 11 12 val output_program : string option -> patriciaLib.term_ptree -> unit 13 14 val encode_psr : string -> string 15 val arm_eval : string -> Term.term -> int -> Thm.thm 16 val print_arm_state : Thm.thm -> unit 17 18 (* Usage: 19 20 * arm_load_from_elf <start address> <elf filename> <ld> 21 e.g. val ld = arm_load_from_elf "0" "a.out" arm_load_empty 22 23 Note: the elf file must be generated with "arm-elf-as -EB ..." and 24 arm-elf-objdump needs to be available at your command line 25 26 * arm_load_from_file <start address> <assembler filename> <ld> 27 e.g. val ld = arm_load_from_file "A00" "code.s" arm_load_empty 28 29 * arm_load_from_string <start address> <code string> <ptree> 30 e.g. val ld = arm_load_from_string "B00" "add r1,r2" arm_load_empty 31 32 * arm_load_from_quote <start address> <code quotation> <ptree> 33 e.g. val ld = arm_load_from_quote "C00" `ascii "hello"` arm_load_empty 34 35 * encode_psr <options> 36 e.g. val s = encode_psr "n=T, q=T, it=0xBA, ge=0xE, t=T, m=fiq" 37 result: val s = "8C0EBA31" : string 38 39 * arm_eval <options> <ptree term> <max cycles> 40 e.g. val prog_def = 41 arm_load_empty 42 |> arm_load_from_string "A00" "thumb\n str r1,[r0],#4" 43 |> fst 44 |> patriciaLib.Define_mk_ptree "prog"; 45 val t = arm_eval "r0=B00, r1=A, pc=A00, cpsr=8C0EBA31" ``prog`` 1; 46 val _ = print_arm_state t 47 48 Note: output is controlled with the trace variable "arm eval" (0--6). 49 *) 50 51end 52