1structure x64_codegen_inputLib :> x64_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->word64`` 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:word64``) 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:word64->word8) a = n2w n`` tm handle e =>
100                     match_term ``n2w n = (f:word64->word8) a`` tm
101         val addr = dest_address (subst i ``a:word64``)
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 = let
129    val (i,_) = match_term ``((m:word64->word64) a)`` tm
130    val addr = dest_address (subst i ``a:word64``)
131    in (ACCESS_WORD,addr) end handle HOL_ERR _ => fail()
132  fun dest_byte_memory tm = let
133    val (i,_) = match_term ``w2w ((m:word64->word8) a)`` tm
134    val addr = dest_address (subst i ``a:word64``)
135    in (ACCESS_BYTE,addr) end handle HOL_ERR _ => fail()
136  fun dest_lsl tm =
137    if not ((fst o dest_const o car o car) tm = "word_lsl") then fail() else
138      ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm)
139  fun dest_lsr tm =
140    if not ((fst o dest_const o car o car) tm = "word_lsr") then fail() else
141      ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm)
142  fun dest_asr tm =
143    if not ((fst o dest_const o car o car) tm = "word_asr") then fail() else
144      ((dest_x o cdr o car) tm, (Arbnum.toInt o numSyntax.dest_numeral o cdr) tm)
145  fun dest_memory_update tm = let
146    val (i,_) = match_term ``(a =+ w) (m:word64->word64)`` tm
147    val addr = dest_address (subst i ``a:word64``)
148    val x = dest_x (subst i ``w:word64``)
149    val _ = if is_var (subst i ``m:word64->word64``) then () else fail()
150    val _ = if is_var (subst i ``w:word64``) then () else fail()
151    in (ACCESS_WORD,addr,x) end handle HOL_ERR _ => let
152    val (i,_) = match_term ``(a =+ n2w n) (m:word64->word64)`` tm
153    val addr = dest_address (subst i ``a:word64``)
154    val x = dest_n2w (subst i ``(n2w n):word64``)
155    val _ = if is_var (subst i ``m:word64->word64``) then () else fail()
156    in (ACCESS_WORD,addr,ASSIGN_X_CONST x) end
157  in ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_REG (dest_reg t2)) handle e =>
158     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_CONST (dest_n2w t2)) handle e =>
159     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_STACK (dest_stack t2)) handle e =>
160     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_BINOP (dest_binop t2)) handle e =>
161     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MONOP (dest_monop t2)) handle e =>
162     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MEMORY (dest_memory t2)) handle e =>
163     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_MEMORY (dest_byte_memory t2)) handle e =>
164     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_LEFT (dest_lsl t2)) handle e =>
165     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_RIGHT (dest_lsr t2)) handle e =>
166     ASSIGN_EXP (dest_reg t1, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (dest_asr t2)) handle e =>
167     ASSIGN_STACK (dest_stack t1, dest_x t2) handle e =>
168     ASSIGN_MEMORY (dest_memory_update t2) handle e =>
169     ASSIGN_OTHER (t1,t2)
170  end
171
172fun term2assign t1 t2 = let
173  fun can_eval (ASSIGN_EXP (_, ASSIGN_EXP_BINOP (ASSIGN_X_CONST _,_,ASSIGN_X_CONST _))) = true
174    | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_MONOP (_, ASSIGN_X_CONST _))) = true
175    | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_LEFT (ASSIGN_X_CONST i,n))) = true
176    | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_RIGHT (ASSIGN_X_CONST i,n))) = true
177    | can_eval (ASSIGN_EXP (_, ASSIGN_EXP_SHIFT_ARITHMETIC_RIGHT (ASSIGN_X_CONST i,n))) = true
178    | can_eval _ = false
179  val t = basic_term2assign t1 t2
180  (* fold constants *)
181  val t = if not (can_eval t) then t else basic_term2assign t1 ((cdr o concl o EVAL) t2)
182  in t end
183
184end;
185