1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
(***********************************************************************)
(* *)
(* Compcert Extensions *)
(* *)
(* Jean-Baptiste Tristan *)
(* *)
(* All rights reserved. This file is distributed under the terms *)
(* described in file ../../LICENSE. *)
(* *)
(***********************************************************************)
open Camlcoq
open Op
open Registers
open Mem
open AST
type ('a,'b) sum = ('a,'b) Datatypes.sum
type instruction =
| Inop
| Iop of operation * reg CList.list * reg
| Iload of memory_chunk * addressing * reg CList.list * reg
| Istore of memory_chunk * addressing * reg CList.list * reg
| Icall of signature * (reg, ident) sum * reg CList.list * reg
| Itailcall of signature * (reg, ident) sum * reg CList.list
| Ialloc of reg * reg
| Icond of condition * reg CList.list
| Ireturn of reg Datatypes.option
type resource = Reg of reg | Mem
let inst_coq_to_caml = function
| RTL.Inop succ -> Inop
| RTL.Iop (op, args, dst, succ) -> Iop (op, args, dst)
| RTL.Iload (chunk, mode, args, dst, succ) -> Iload (chunk, mode, args, dst)
| RTL.Istore (chunk, mode, args, src, succ) -> Istore (chunk, mode, args, src)
| RTL.Icall (sign, id, args, dst, succ) -> Icall (sign, id, args, dst)
| RTL.Itailcall (sign, id, args) -> Itailcall (sign, id, args)
| RTL.Ialloc (dst, size, succ) -> Ialloc (dst, size)
| RTL.Icond (cond, args, succ1, succ2) -> Icond (cond, args)
| RTL.Ireturn (res) -> Ireturn (res)
let inst_caml_to_coq i (links : RTL.node list) =
match i,links with
| Inop,[p] -> RTL.Inop p
| Iop (op, args, dst),[p] -> RTL.Iop (op, args, dst,p)
| Iload (chunk, mode, args, dst),[p] -> RTL.Iload (chunk, mode, args,dst,p)
| Istore (chunk, mode, args, src),[p] -> RTL.Istore (chunk, mode, args, src,p)
| Icall (sign, id, args, dst),[p] -> RTL.Icall (sign, id, args, dst,p)
| Itailcall (sign, id, args),[] -> RTL.Itailcall (sign, id, args)
| Ialloc (dst, size),[p] -> RTL.Ialloc (dst, size,p)
| Icond (cond, args),[p1;p2] -> RTL.Icond (cond,args,p1,p2)
| Ireturn (res),[] -> RTL.Ireturn res
| _,_ -> failwith "Echec lors de la conversion des instrucitons internes vers compcert"
let print_inst node = string_of_int (snd node)
let to_int = fun n -> Int32.to_int (camlint_of_positive n)
let to_binpos = fun n -> positive_of_camlint (Int32.of_int n)
let rec string_of_args args =
match args with
| CList.Coq_nil -> ""
| CList.Coq_cons (arg,args) -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args
let string_of_z z = string_of_int (Int32.to_int (Camlcoq.camlint_of_z z))
let string_of_comparison = function
| Integers.Ceq -> "eq"
| Integers.Cne -> "ne"
| Integers.Clt -> "lt"
| Integers.Cle -> "le"
| Integers.Cgt -> "gt"
| Integers.Cge -> "ge"
let string_of_cond = function
| Ccomp c -> Printf.sprintf "comp %s" (string_of_comparison c)
| Ccompu c -> Printf.sprintf "compu %s" (string_of_comparison c)
| Ccompimm (c,i) -> Printf.sprintf "compimm %s %s" (string_of_comparison c) (string_of_z i)
| Ccompuimm (c,i) -> Printf.sprintf "compuimm %s %s" (string_of_comparison c) (string_of_z i)
| Ccompf c -> Printf.sprintf "compf %s" (string_of_comparison c)
| Cnotcompf c -> Printf.sprintf "notcompf %s" (string_of_comparison c)
| Cmaskzero i -> Printf.sprintf "maskzero %s" (string_of_z i)
| Cmasknotzero i -> Printf.sprintf "masknotzero %s" (string_of_z i)
let string_of_op = function
| Omove -> "move"
| Ointconst i -> Printf.sprintf "intconst %s" (string_of_z i)
| Ofloatconst f -> Printf.sprintf "floatconst %s" (string_of_float f)
| Oaddrsymbol (id,i) -> Printf.sprintf "addrsymbol %s %s" (string_of_int (to_int id)) (string_of_z i)
| Oaddrstack i -> Printf.sprintf "addrstack %s" (string_of_z i)
| Ocast8signed -> "cast8signed"
| Ocast8unsigned -> "cast8unsigned"
| Ocast16signed -> "cast16signed"
| Ocast16unsigned -> "cast16unsigned"
| Oadd -> "add"
| Oaddimm i -> Printf.sprintf "addimm %s" (string_of_z i)
| Osub -> "sub"
| Osubimm i -> Printf.sprintf "subimm %s" (string_of_z i)
| Omul -> "mul"
| Omulimm i -> Printf.sprintf "mulimm %s" (string_of_z i)
| Odiv -> "div"
| Odivu -> "divu"
| Oand -> "and"
| Oandimm i -> Printf.sprintf "andimm %s" (string_of_z i)
| Oor -> "or"
| Oorimm i -> Printf.sprintf "orimm %s" (string_of_z i)
| Oxor -> "xor"
| Oxorimm i -> Printf.sprintf "xorimm %s" (string_of_z i)
| Onand -> "nand"
| Onor -> "nor"
| Onxor -> "nxor"
| Oshl -> "shl"
| Oshr -> "shr"
| Oshrimm i -> Printf.sprintf "shrimm %s" (string_of_z i)
| Oshrximm i -> Printf.sprintf "shrximm %s" (string_of_z i)
| Oshru -> "shru"
| Orolm (i,j) -> Printf.sprintf "rolm %s %s" (string_of_z i) (string_of_z j)
| Onegf -> "negf"
| Oabsf -> "absf"
| Oaddf -> "addf"
| Osubf -> "subf"
| Omulf -> "mulf"
| Odivf -> "divf"
| Omuladdf -> "muladdf"
| Omulsubf -> "mulsubf"
| Osingleoffloat -> "singleoffloat"
| Ointoffloat -> "intoffloat"
| Ointuoffloat -> "intuoffloat"
| Ofloatofint -> "floatofint"
| Ofloatofintu -> "floatofintu"
| Ocmp c -> Printf.sprintf "cmpcmpcmp"
let rec to_coq_list = function
| [] -> CList.Coq_nil
| e :: l -> CList.Coq_cons (e,(to_coq_list l))
let rec to_caml_list = function
| CList.Coq_nil -> []
| CList.Coq_cons (e,l) -> e :: to_caml_list l
|
