1structure SALGen :> SALGen = 2struct 3 4(* Interactive 5quietdec := true; 6app load ["pairLib","basic", "SALTheory"]; 7open pairLib pairSyntax PairRules numSyntax basic SALTheory; 8quietdec := false; 9*) 10 11open HolKernel Parse boolLib pairLib pairSyntax bossLib ; 12open PairRules numSyntax basic SALTheory; 13 14val ERR = mk_HOL_ERR "SALGen"; 15 16(* --------------------------------------------------------------------*) 17(* Generate SAL code for a FIL program *) 18(* --------------------------------------------------------------------*) 19 20structure M = Binarymap 21structure S = Binaryset 22val VarType = ref (Type `:word32`) (* numSyntax.num *) 23 24(* --------------------------------------------------------------------*) 25(* Datatypes, Commonly-used variables and functions *) 26(* --------------------------------------------------------------------*) 27 28val nop = prim_mk_const{Name="NOP",Thy="SAL"}; 29val reduce_tm = prim_mk_const{Name="Reduce",Thy="SAL"}; 30val union_tm = prim_mk_const{Name="UNION",Thy="SAL"}; 31val asg_tm = prim_mk_const{Name="ASG",Thy="SAL"}; 32val ifgoto_tm = prim_mk_const{Name="IFGOTO",Thy="SAL"}; 33val goto_tm = prim_mk_const{Name="GOTO",Thy="SAL"}; 34 35fun dest_composite ty = 36 case total dest_thy_type ty 37 of SOME {Tyop="COMPOSITE",Thy="SAL",Args=[x]} => x 38 | other => raise ERR "dest_composite" ""; 39 40(* --------------------------------------------------------------------*) 41(* Auxiliary functions manipulating labels *) 42(* --------------------------------------------------------------------*) 43 44val label_tm = prim_mk_const{Name="L",Thy="SAL"}; 45 46fun mk_label i = mk_comb(label_tm, term_of_int i); 47 48val label_index = ref 0; 49 50fun reset_label () = label_index := 0 51fun cur_label() = mk_label (!label_index) 52 53fun next_label () = 54 let val _ = label_index := !label_index + 1; 55 in 56 mk_label (!label_index) 57 end; 58 59(* ---------------------------------------------------------------------*) 60(* Mechanism for mechanical reasoning *) 61(* A specification stores all information about a FIL program including *) 62(* a theorem stating that the SAL code "implements" the FIL program. *) 63(* The composition of specifications is directed by the syntax of the *) 64(* program and goes in a bottom-up manner. *) 65(* ---------------------------------------------------------------------*) 66 67type spec_type = {body : term, dst : term, entry : term, exit : term, exp : term, thm : thm} 68 69(* Make a basic specification for single assignment instruction *) 70 71fun mk_instr_spec (entry_l,exit_l) (dest,src) = 72 let 73 val ty = type_of dest 74 val value = mk_pair (src, dest) 75 val instr = list_mk_comb (inst [alpha |-> ty] asg_tm, [entry_l, dest, src, exit_l]) 76 val s = list_mk_pair [entry_l, instr, exit_l] 77 val spec = list_mk_comb(inst [alpha |-> ty] reduce_tm, [s, value]) 78 val spec_thm = prove(spec, SIMP_TAC std_ss [inst_rule]) 79 in 80 {entry = entry_l, exit = exit_l, body = instr, thm = spec_thm, exp = src, dst = dest} 81 end 82 83(* Union of two structures (i.e. sequential composition *) 84 85fun mk_union_spec (spec1:spec_type) (spec2:spec_type) = 86 let (* s1 |+| s2 *) 87 val union_body = list_mk_comb(inst [alpha |-> !VarType] union_tm, [#body spec1, #body spec2]) 88 val exp = mk_plet (#dst spec1, #exp spec1, 89 mk_comb(mk_pabs (#dst spec1, #exp spec2), #dst spec1)) 90 val value = mk_pair(exp, #dst spec2) 91 val s = list_mk_pair [#entry spec1, union_body, #exit spec2] 92 val spec = list_mk_comb(inst [alpha |-> !VarType] reduce_tm, [s, value]) 93 94 val spec_lem = prove (spec, (* set_goal ([], spec) *) 95 MATCH_MP_TAC seq_rule THEN 96 EXISTS_TAC (#exit spec1) THEN EXISTS_TAC (#dst spec1) THEN 97 PBETA_TAC THEN 98 REWRITE_TAC [#thm spec1, #thm spec2] 99 ) 100 val spec_thm = PBETA_RULE spec_lem 101 in 102 {entry = #entry spec1, exit = #exit spec2, body = union_body, thm = spec_thm, exp = exp, dst = #dst spec2} 103 end 104 105(* --------------------------------------------------------------------*) 106(* Eliminate the deepest "let" expression. It is for optiomization. *) 107(* --------------------------------------------------------------------*) 108 109val ELIM_DEEP_LET_CONV = 110 let 111 val elim_deep_let_conv = (fn t => (DEPTH_CONV (SIMP_CONV bool_ss [Once LET_THM])) t) 112 in 113 RATOR_CONV elim_deep_let_conv THENC 114 RAND_CONV elim_deep_let_conv 115 end; 116 117(* --------------------------------------------------------------------*) 118(* Compose the specifications in a bottom-up manner. *) 119(* --------------------------------------------------------------------*) 120 121(* Generate specification for conditional structures. *) 122 123fun mk_cond_spec (entry_l,exit_l) (dest,src) args = 124 let 125 val (J,M1,M2) = dest_cond src 126 127 val args = hd(free_vars J) 128 val c = mk_pabs(args,J) 129 val (l1,l2,l3,l4) = (entry_l,next_label(),next_label(),exit_l) 130 val ifgoto = list_mk_comb(inst [alpha |-> !VarType] ifgoto_tm, [l1, c, l2, l3]) 131 val spec1 = gen_code (l2,M1,l4) (args,dest) 132 val spec2 = gen_code (l3,M2,l4) (args,dest) 133 134 val b1 = list_mk_comb(inst [alpha |-> !VarType] union_tm, [ifgoto, #body spec1]) 135 val b2 = list_mk_comb(inst [alpha |-> !VarType] union_tm, [b1, #body spec2]) 136 val s = list_mk_pair [l1, b2, l4] 137 138 val exp = mk_cond (mk_comb(c,args), 139 mk_comb(mk_pabs(args, #exp spec1), args), 140 mk_comb(mk_pabs(args, #exp spec2), args)) 141 val value = mk_pair(exp, dest) 142 val spec = list_mk_comb(inst [alpha |-> !VarType] reduce_tm, [s, value]) 143 144 val spec_lem = prove (spec, (* set_goal ([], spec) *) 145 MATCH_MP_TAC CONDITIONAL_RULE THEN 146 PBETA_TAC THEN 147 REWRITE_TAC [#thm spec1, #thm spec2] 148 ) 149 val spec_thm = PBETA_RULE spec_lem 150 val exp' = mk_cond (J, #exp spec1, #exp spec2) 151 152(* val t = #1 (dest_pair (List.last (#2 (strip_comb (concl spec_lem1))))) 153 val lem = ELIM_DEEP_LET_CONV t handle _ => REFL t 154 val spec_thm = ONCE_REWRITE_RULE [lem] spec_lem1 155*) 156 in 157 {entry = entry_l, exit = exit_l, body = b2, thm = spec_thm, exp = exp', dst = dest} 158 end 159 160and 161 162(* The composition is syntax directed. *) 163 164mk_spec (entry_l,exit_l) (dest,src) args = 165 if is_atomic src orelse is_pair src then 166 mk_instr_spec (entry_l,exit_l) (dest,src) 167 168 else if is_cond src then (* t = if P then M else N *) 169 mk_cond_spec (entry_l,exit_l) (dest,src) args 170 171 else if is_comb src then 172 let val (operator, operands) = strip_comb src 173 in 174 if basic.is_binop operator then (* Arith. and Logical Operations *) 175 mk_instr_spec (entry_l,exit_l) (dest,src) 176 else (* Application *) 177 raise Fail "unimplemented SAL code generation for function applications" 178 end 179 else 180 raise Fail "unimplemented for this structure!" 181 182and 183 184(* Code generation (by producing specifications) *) 185 186gen_code (entry_l, t, exit_l) (input,output) = 187 if is_atomic t orelse is_pair t then 188 if t = output then (* no copying is required *) 189 {entry = entry_l, exit = exit_l, body = inst [alpha |-> !VarType] nop, exp = t, dst = t, 190 thm = dummy_rule} 191 else mk_instr_spec (entry_l,exit_l) (output, t) 192 193 else if is_let t then (* exp = LET (\v. N) M *) 194 let 195 val (v,M,N) = dest_plet t 196 val new_l = next_label() 197 val spec1 = mk_spec (entry_l,new_l) (v,M) input 198 val spec2 = gen_code (new_l, N, exit_l) (#dst spec1, output) 199 val spec3 = if #body spec2 = (inst [alpha |-> !VarType] nop) then 200 mk_spec (entry_l,exit_l) (v,M) input (* make sure the exit label is correct *) 201 else mk_union_spec spec1 spec2 202 in 203 spec3 204 end 205 206 else 207 {entry = entry_l, exit = exit_l, body = t, thm = mk_thm ([],``T``), exp = t, dst = t} 208 ; 209 210(* --------------------------------------------------------------------*) 211(* Fromat SAL programs for printing. *) 212(* --------------------------------------------------------------------*) 213 214val seperator = ref ("\n") (* " \n " *) 215val indent = " " 216 217fun format_label l = 218 "l" ^ (term_to_string (#2 (dest_comb l))) handle _ => term_to_string l 219 220fun indent_label l = 221 let val label = format_label(l) 222 in case (size (label)) of 223 2 => label ^ ": " | 224 3 => label ^ ": " | 225 4 => label ^ ": " | 226 _ => label ^ ":" 227 end 228 229(* Turn a piece of SAL code into a string *) 230 231fun formatSAL code = 232 if is_const code andalso #1 (dest_const code) = "NOP" then "" 233 else if is_atomic code orelse is_pair code then term_to_string code 234 else if is_comb code then 235 let val (operator, xs) = strip_comb code 236 val op_s = #1 (dest_const operator) 237 in 238 if op_s = "UNION" then 239 formatSAL (hd xs) ^ formatSAL (hd (tl xs)) 240 else if op_s = "ASG" then 241 let val [entry_l, dest, src, exit_l] = xs 242 in indent_label entry_l ^ term_to_string dest ^ " := " ^ term_to_string src ^ 243 " (goto " ^ format_label exit_l ^ ")" ^ !seperator 244 end 245 else if op_s = "IFGOTO" then 246 let val [entry_l, cond, true_l, false_l] = xs 247 in indent_label entry_l ^ "ifgoto " ^ 248 term_to_string (#2 (dest_pabs cond)) ^ " " ^ format_label true_l ^ 249 " " ^ format_label false_l ^ !seperator 250 end 251 else if op_s = "GOTO" then 252 let val [entry_l, exit_l] = xs 253 in indent ^ "goto " ^ format_label exit_l ^ !seperator 254 end 255 else 256 term_to_string code 257 end 258 else 259 term_to_string code 260 261(* --------------------------------------------------------------------*) 262(* Pre-processing before code generation *) 263(* --------------------------------------------------------------------*) 264 265(* Find the output of an expression *) 266 267fun find_output t = 268 if is_let t then 269 let val (v,M,N) = dest_plet t 270 in if is_atomic N orelse is_pair N then SOME N 271 else find_output N 272 end 273 else if is_cond t then NONE 274 else if is_pabs t then 275 find_output (#2 (dest_pabs t)) 276 else NONE 277 278(* Identify the argument, body and the output of a function *) 279 280fun pre_process def = 281 let 282 val (fname, fbody) = dest_eq (concl (SPEC_ALL def)) 283 val fname = if is_comb fname then #1 (dest_comb fname) else fname 284 val (args,body) = dest_pabs fbody handle _ => (#2 (dest_comb fname), fbody) 285 286 val (body, output) = 287 case find_output(body) of 288 SOME x => (body, x) | 289 NONE => (mk_plet(args, body, args), args) 290 in 291 {body = body, input = args, output = output} 292 end 293 294(* --------------------------------------------------------------------*) 295(* Certifing Code Generation *) 296(* --------------------------------------------------------------------*) 297 298val printSAL = print o formatSAL; 299 300fun certified_gen def = 301 let 302 val rs = pre_process def 303 val (sane,var_type) = pre_check(#input rs, #body rs) 304 in 305 if sane then 306 let val _ = (reset_label(); VarType := var_type) 307 val s = gen_code (next_label(), #body rs, next_label()) (#input rs, #output rs) 308 in 309 {code = #body s, thm = #thm s} 310 end 311 handle _ => 312 ( print("STOP: The source program (FIL) includes structures whose conversion hasn't been implemented!\n"); 313 {code = nop, thm = mk_thm ([], Term`T`)} 314 ) 315 else 316 ( print("STOP: The source program (FIL) is invalid! (e.g. all variables are not of the same type)\n"); 317 {code = nop, thm = mk_thm ([], Term`T`)} 318 ) 319 end 320 321(* --------------------------------------------------------------------*) 322 323end (* struct *) 324