1structure codegen_inputLib :> codegen_inputLib =
2struct
3
4open HolKernel boolLib bossLib Parse;
5open helperLib wordsTheory;
6
7
8(* core code generator input syntax *)
9
10datatype access_type =
11    ACCESS_WORD
12  | ACCESS_BYTE;
13
14datatype assign_address_type =
15    ASSIGN_ADDRESS_REG of int
16  | ASSIGN_ADDRESS_OFFSET_ADD of int * Arbnum.num
17  | ASSIGN_ADDRESS_OFFSET_SUB of int * Arbnum.num;
18
19datatype assign_monop_type =
20    ASSIGN_MONOP_NOT
21  | ASSIGN_MONOP_NEG;
22
23datatype assign_binop_type =
24    ASSIGN_BINOP_ADD
25  | ASSIGN_BINOP_SUB
26  | ASSIGN_BINOP_MUL
27  | ASSIGN_BINOP_MOD
28  | ASSIGN_BINOP_DIV
29  | ASSIGN_BINOP_AND
30  | ASSIGN_BINOP_XOR
31  | ASSIGN_BINOP_OR;
32
33datatype assign_x_type =
34    ASSIGN_X_REG of int          (* register number *)
35  | ASSIGN_X_CONST of Arbnum.num (* constant *);
36
37datatype assign_exp_type =
38    ASSIGN_EXP_REG of int
39  | ASSIGN_EXP_CONST of Arbnum.num  (* constant *)
40  | ASSIGN_EXP_STACK of int         (* stack[offset] *)
41  | ASSIGN_EXP_BINOP of assign_x_type * assign_binop_type * assign_x_type
42  | ASSIGN_EXP_MONOP of assign_monop_type * assign_x_type
43  | ASSIGN_EXP_MEMORY of access_type * assign_address_type
44  | ASSIGN_EXP_SHIFT_LEFT of assign_x_type * int
45  | ASSIGN_EXP_SHIFT_RIGHT of assign_x_type * int
46  | ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT of assign_x_type * int
47
48datatype assign_type =
49    ASSIGN_EXP of int * assign_exp_type        (* register := expression *)
50  | ASSIGN_STACK of int * assign_x_type        (* stack[offset] := x *)
51  | ASSIGN_MEMORY of access_type * assign_address_type * assign_x_type
52                                               (* mem[address] := x *)
53  | ASSIGN_OTHER of term * term                (* lhs := rhs *);
54
55datatype guard_compare_type =
56    GUARD_COMPARE_LESS of bool       (* true: signed, false: unsigned *)
57  | GUARD_COMPARE_LESS_EQUAL of bool (* true: signed, false: unsigned *)
58  | GUARD_COMPARE_EQUAL;
59
60datatype guard_type =
61    GUARD_NOT of guard_type
62  | GUARD_COMPARE of int * guard_compare_type * assign_x_type  (* reg, cmp, reg/const *)
63  | GUARD_EQUAL_BYTE of assign_address_type * Arbnum.num
64  | GUARD_TEST of int * assign_x_type
65  | GUARD_OTHER of term;
66
67
68(* term2guard, term2assign *)
69
70fun dest_var_char c tm =
71  if not ((hd o explode o fst o dest_var) tm = c) then fail() else
72    (string_to_int o implode o tl o explode o fst o dest_var) tm
73val dest_reg = dest_var_char #"r"
74val dest_stack = dest_var_char #"s"
75fun dest_n2w tm = if car tm = ``n2w:num->word32`` then numSyntax.dest_numeral (cdr tm) else fail()
76fun dest_n2w_byte tm = if car tm = ``n2w:num->word8`` then numSyntax.dest_numeral (cdr tm) else fail()
77fun dest_x tm = ASSIGN_X_REG (dest_reg tm) handle e => ASSIGN_X_CONST (dest_n2w tm)
78fun dest_address tm = ASSIGN_ADDRESS_REG (dest_reg tm) handle e =>
79  (if not ((fst o dest_const o car o car) tm = "word_add") then fail() else
80    ASSIGN_ADDRESS_OFFSET_ADD ((dest_reg o cdr o car) tm, dest_n2w (cdr tm))) handle e =>
81  if not ((fst o dest_const o car o car) tm = "word_sub") then fail() else
82    ASSIGN_ADDRESS_OFFSET_SUB ((dest_reg o cdr o car) tm, dest_n2w (cdr tm))
83
84fun basic_term2guard tm = (* expects input to use "~", "<+", "<" and "=" only *)
85  if can dest_neg tm then GUARD_NOT (basic_term2guard (dest_neg tm)) else let
86    val cmps = [("word_lo", (GUARD_COMPARE_LESS false, GUARD_COMPARE_LESS_EQUAL false)),
87                ("word_lt", (GUARD_COMPARE_LESS true, GUARD_COMPARE_LESS_EQUAL true)),
88                ("=", (GUARD_COMPARE_EQUAL, GUARD_COMPARE_EQUAL))]
89    val (d1,d2) = (snd o hd o filter (fn x => fst x = (fst o dest_const o car o car) tm)) cmps
90    val x1 = (cdr o car) tm
91    val x2 = cdr tm
92    in if can (match_term ``x && y = 0w:word32``) tm then
93         GUARD_TEST ((dest_reg o cdr o car o cdr o car) tm, (dest_x o cdr o cdr o car) tm)
94       else if can dest_n2w x1 then
95         GUARD_NOT (GUARD_COMPARE (dest_reg x2, d2, dest_x x1))
96       else
97         GUARD_COMPARE (dest_reg x1, d1, dest_x x2)
98       handle e => let
99         val (i,_) = match_term ``(f:word32->word8) a = n2w n`` tm handle e =>
100                     match_term ``n2w n = (f:word32->word8) a`` tm
101         val addr = dest_address (subst i ``a:word32``)
102         val imm = dest_n2w_byte (subst i ``(n2w n):word8``)
103         in GUARD_EQUAL_BYTE (addr,imm) end
104       handle e =>
105         GUARD_OTHER tm
106    end;
107
108fun term2guard tm = let
109  fun f (GUARD_NOT (GUARD_NOT x)) = x | f x = x
110  val c = REWRITE_CONV [WORD_HIGHER,WORD_GREATER,WORD_HIGHER_EQ,
111    WORD_GREATER_EQ,GSYM WORD_NOT_LOWER,GSYM WORD_NOT_LESS]
112  val tm = ((snd o dest_eq o concl o c) tm) handle e => tm
113  in f (basic_term2guard tm) end;
114
115fun basic_term2assign t1 t2 = let
116  val binops = [("word_add",ASSIGN_BINOP_ADD), ("word_sub",ASSIGN_BINOP_SUB),
117                ("word_mul",ASSIGN_BINOP_MUL), ("word_and",ASSIGN_BINOP_AND),
118                ("word_div",ASSIGN_BINOP_DIV), ("word_mod",ASSIGN_BINOP_MOD),
119                ("word_xor",ASSIGN_BINOP_XOR), ("word_or",ASSIGN_BINOP_OR)]
120  val monops = [("word_1comp",ASSIGN_MONOP_NOT), ("word_2comp",ASSIGN_MONOP_NEG)]
121  fun dest_binop tm =
122    ((dest_x o cdr o car) tm,
123     (snd o hd o filter (fn x => fst x = (fst o dest_const o car o car) tm)) binops,
124     (dest_x o cdr) tm)
125  fun dest_monop tm =
126    ((snd o hd o filter (fn x => fst x = (fst o dest_const o car) tm)) monops,
127     (dest_x o cdr) tm)
128  fun dest_memory tm =
129    if not (is_var (car tm) andalso type_of (car tm) = ``:word32->word32``) then fail() else
130      (ACCESS_WORD,dest_address (cdr tm))
131  fun dest_byte_memory tm =
132    if not (is_const (car tm) andalso type_of (car tm) = ``:word8->word32``) then fail() else
133      (ACCESS_BYTE,dest_address (cdr (cdr tm)))
134  fun dest_lsl tm =
135    if not ((fst o dest_const o car o car) tm = "word_lsl") then fail() else
136      ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm)
137  fun dest_lsr tm =
138    if not ((fst o dest_const o car o car) tm = "word_lsr") then fail() else
139      ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm)
140  fun dest_asr tm =
141    if not ((fst o dest_const o car o car) tm = "word_asr") then fail() else
142      ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm)
143  fun dest_memory_update tm = let
144    val (i,_) = match_term ``(a =+ w) (m:word32->word32)`` tm
145    val addr = dest_address (subst i ``a:word32``)
146    val x = dest_x (subst i ``w:word32``)
147    val _ = if is_var (subst i ``m:word32->word32``) then () else fail()
148    val _ = if is_var (subst i ``w:word32``) then () else fail()
149    in (ACCESS_WORD,addr,x) end handle HOL_ERR _ => let
150    val (i,_) = match_term ``(a =+ w2w (w:word32)) (m:word32->word8)`` tm
151    val addr = dest_address (subst i ``a:word32``)
152    val x = dest_x (subst i ``w:word32``)
153    val _ = if is_var (subst i ``m:word32->word8``) then () else fail()
154    val _ = if is_var (subst i ``w:word32``) then () else fail()
155    in (ACCESS_BYTE,addr,x) end handle HOL_ERR _ => let
156    val (i,_) = match_term ``(a =+ n2w n) (m:word32->word8)`` tm
157    val addr = dest_address (subst i ``a:word32``)
158    val x = dest_n2w_byte (subst i ``(n2w n):word8``)
159    val _ = if is_var (subst i ``m:word32->word8``) then () else fail()
160    in (ACCESS_BYTE,addr,ASSIGN_X_CONST x) end handle HOL_ERR _ => let
161    val (i,_) = match_term ``(a =+ n2w n) (m:word32->word32)`` tm
162    val addr = dest_address (subst i ``a:word32``)
163    val x = dest_n2w (subst i ``(n2w n):word32``)
164    val _ = if is_var (subst i ``m:word32->word32``) then () else fail()
165    in (ACCESS_WORD,addr,ASSIGN_X_CONST x) end
166  in ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_REG (dest_reg t2)) handle e =>
167     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_CONST (dest_n2w t2)) handle e =>
168     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_STACK (dest_stack t2)) handle e =>
169     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_BINOP (dest_binop t2)) handle e =>
170     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MONOP (dest_monop t2)) handle e =>
171     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MEMORY (dest_memory t2)) handle e =>
172     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MEMORY (dest_byte_memory t2)) handle e =>
173     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_LEFT (dest_lsl t2)) handle e =>
174     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_RIGHT (dest_lsr t2)) handle e =>
175     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (dest_asr t2)) handle e =>
176     ASSIGN_STACK (dest_stack t1, dest_x t2) handle e =>
177     ASSIGN_MEMORY (dest_memory_update t2) handle e =>
178     ASSIGN_OTHER (t1,t2)
179  end
180
181fun term2assign t1 t2 = let
182  fun can_eval (ASSIGN_EXP (_, ASSIGN_EXP_BINOP (ASSIGN_X_CONST _,_,ASSIGN_X_CONST _))) = true
183    | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_MONOP (_, ASSIGN_X_CONST _))) = true
184    | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_LEFT (ASSIGN_X_CONST i,n))) = true
185    | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_RIGHT (ASSIGN_X_CONST i,n))) = true
186    | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (ASSIGN_X_CONST i,n))) = true
187    | can_eval _ = false
188  val t = basic_term2assign t1 t2
189  (* fold constants *)
190  val t = if not (can_eval t) then t else basic_term2assign t1 ((cdr o concl o EVAL) t2)
191  in t end
192
193end;
194