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