1structure m1_progLib :> m1_progLib =
2struct
3
4open HolKernel boolLib bossLib;
5
6open decompilerLib;
7open m1_progTheory helperLib sexpTheory pairSyntax;
8open combinTheory addressTheory sexpTheory imported_acl2Theory;
9open complex_rationalTheory hol_defaxiomsTheory;
10open arithmeticTheory;
11
12
13(* m1_spec produces Hoare triple theorems for M1 instructions *)
14
15fun m1_spec s = let
16  val m1_thms = [M1_ICONST,M1_ILOAD,M1_ISTORE,M1_IADD,M1_ISUB,M1_IMUL,M1_GOTO,M1_IFLE];
17  val tm = Parse.Term [QUOTE s]
18  fun match_thm th = let
19    val (_,_,c,_) = helperLib.dest_spec (concl th)
20    val c = c |> rator |> rand |> rand
21    val m = fst (match_term c tm)
22    in INST m th end
23  val th = match_thm (first (can match_thm) m1_thms)
24  val pc_offset =
25    th |> concl |> rand |> rand |> rand |> rand |> rand
26       |> (fn x => numSyntax.int_of_term x handle HOL_ERR _ =>
27                   Arbint.toInt(intSyntax.int_of_term x))
28  val th = let
29    val pat = find_term (can (match_term ``tL a v``)) (concl th)
30    val (v,ty) = dest_var(rand pat)
31    val n = Arbnum.toInt(numSyntax.dest_numeral (rand (rator pat)))
32    val s = [mk_var(v,ty) |-> mk_var("v"^(int_to_string n),ty)]
33    in INST s th end handle HOL_ERR _ => th
34  in if can (find_term (fn x => x = ``"IFLE"``)) (concl th) then
35       ((th,1,SOME pc_offset),SOME (match_thm M1_IFLE_NOP,1,SOME 1))
36     else ((th,1,SOME pc_offset),NONE) end;
37
38val m1_status = TRUTH
39val m1_pc = ``PC``;
40fun m1_jump (tm1:term) (tm2:term) (jump_length:int) (forward:bool) = ("",0)
41
42val m1_tools = (m1_spec, m1_jump, m1_status, m1_pc)
43
44
45(* the decompiler is specialised to deal with s-expressions and the M1 model *)
46
47fun dest_tuple tm =
48  let val (x,y) = pairSyntax.dest_pair tm in x :: dest_tuple y end handle HOL_ERR e => [tm];
49
50fun fix_pc y th = let
51    val format = ``add p (nat n)``
52    val fixed_pc = subst [mk_var("n",``:num``)|->numSyntax.term_of_int y] format
53    val thi = INST [mk_var("p",``:sexp``)|->fixed_pc] th
54    val thi = SIMP_RULE std_ss [add_nat,add_nat_int,add_ASSOC] thi
55    in thi end;
56
57val prev = ref (TRUTH,TRUTH);
58val (res,def) = !prev
59fun sexp_finalise_decompile (res,def) = let
60  val _ = (prev := (res,def))
61  val _ = echo 2 " - converting to produce sexp\n"
62  fun sexp_result output = let
63    fun ff [] = (fst o dest_eq o concl) nil_def
64      | ff (v::vs) = mk_comb(mk_comb(``cons``,v),ff vs)
65    in mk_pabs(output,ff (dest_tuple output)) end;
66  val fhd = hd (CONJUNCTS def)
67  val f = last (CONJUNCTS def)
68  val (tm1,tm2) = (dest_eq o concl o SPEC_ALL) f
69  val input = cdr tm1
70  val name = (fst o dest_const o car) tm1
71  val name = ("sexp_" ^ name)
72  val output = get_output_list f
73  val fix = sexp_result output
74  fun ff [] = "sexp"
75    | ff (x::xs) = "sexp -> " ^ ff xs
76  val ty = Parse.Type [QUOTE (":" ^ ff (dest_tuple input))]
77  val tm = mk_var(name,ty)
78  fun hh tm [] = tm
79    | hh tm (x::xs) = hh (mk_comb(tm,x)) xs
80  val lhs = hh tm (dest_tuple input)
81  val eq_tm = mk_eq (lhs,mk_comb(fix,tm1))
82  val def3 = new_definition(name,eq_tm)
83  val new_lhs = (fst o dest_eq o concl o SPEC_ALL) def3
84  fun rw (FUN_LET (x,y,t)) = FUN_LET (x, y, rw t)
85    | rw (FUN_IF (x,t1,t2)) = FUN_IF (x, rw t1, rw t2)
86    | rw (FUN_COND (x,t)) = FUN_COND (x, rw t)
87    | rw (FUN_VAL tm) =
88        if tm = tm1 then FUN_VAL new_lhs
89        else FUN_VAL (snd (dest_pabs fix))
90  val tm3 = ftree2tm (rw (tm2ftree tm2))
91  val goal = mk_eq(new_lhs,tm3)
92  val inferred = prove(goal,
93    REWRITE_TAC [def3]
94    THEN CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [f]))
95    THEN REPEAT (AUTO_DECONSTRUCT_TAC cdr)
96    THEN SIMP_TAC std_ss []
97    THEN CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV)
98    THEN SIMP_TAC std_ss [])
99  val def2 = REWRITE_RULE [ite_intro] inferred
100  val tm7 = cdr tm1
101  fun ff [] = [] | ff (v::vs) = let
102    in [``car``] :: map (fn y => y @ [``cdr``]) (ff vs) end
103  fun g [] = ``value:sexp``
104    | g (x::xs) = mk_comb(x,g xs)
105  val tm8 = list_mk_pair (map g (ff (dest_tuple (output))))
106  val tm9 = mk_anylet([(``value:sexp``,(fst o dest_eq o concl o SPEC_ALL) def3)],tm8)
107  val goal = mk_eq (tm1,tm9)
108  val rw_thm = prove(goal,
109    SIMP_TAC std_ss [def3,LET_DEF]
110    THEN CONV_TAC (DEPTH_CONV FORCE_PBETA_CONV)
111    THEN SIMP_TAC std_ss [car_def,cdr_def])
112  val res = REWRITE_RULE [rw_thm] res
113  (* flatten let-expressions, leave no ``let ... = (let ... in ..) in ...`` *)
114  fun flatten (FUN_IF (x,t1,t2)) = FUN_IF (x, flatten t1, flatten t2)
115    | flatten (FUN_COND (x,t)) = FUN_COND (x, flatten t)
116    | flatten (FUN_VAL tm) = FUN_VAL tm
117    | flatten (FUN_LET (x,y,t)) = let
118       val (tm1,tm2) = dest_let y
119       val (v,tm1) = dest_abs tm1
120       val xs = (v,tm2) :: Lib.zip (dest_tuple x) (dest_tuple tm1)
121       in foldr (fn ((x,y),z) => FUN_LET (x,y,z)) (flatten t) xs end
122       handle HOL_ERR _ => FUN_LET (x,y,flatten t)
123  val (tm10,tm11) = (dest_eq o concl o SPEC_ALL) def2
124  val tm12 = ftree2tm (flatten (tm2ftree tm11))
125  val goal = mk_eq(tm10,tm12)
126  val def2 = prove(goal,
127    CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [def2]))
128    THEN SIMP_TAC std_ss [LET_DEF])
129  val def2 = REWRITE_RULE [ite_intro] def2
130  val def2 = SIMP_RULE bool_ss [top_defun,pop_defun,push_defun,nth_lemma,
131       LET_DEF,nth_1,cdr_def,car_def,ite_def,not_eq_nil] def2
132  val def2 = REWRITE_RULE [ite_intro] def2
133  in (res,def2) end;
134
135val _ = (decompiler_set_pc := fix_pc);
136val _ = (decompiler_finalise := sexp_finalise_decompile)
137
138val decompile_m1 = decompile m1_tools
139
140end
141
142
143