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
|
(***********************************************************************)
(* *)
(* 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 Memory
open Mem
open AST
type ('a,'b) sum = ('a,'b) Datatypes.sum
type instruction =
| Inop
| Iop of operation * reg list * reg
| Iload of memory_chunk * addressing * reg list * reg
| Istore of memory_chunk * addressing * reg list * reg
| Icall of signature * (reg, ident) sum * reg list * reg
| Itailcall of signature * (reg, ident) sum * reg list
| Icond of condition * reg list
| Ireturn of reg 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.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)
| 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 -> P.to_int n
let to_binpos = fun n -> P.of_int n
let rec string_of_args args =
match args with
| [] -> ""
| arg :: args -> "r" ^ (string_of_int (to_int arg)) ^ " " ^ string_of_args args
let string_of_z z = string_of_int (Z.to_int 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 (camlfloat_of_coqfloat32 f))
| Ocast8signed -> "cast8signed"
| Ocast8unsigned -> "cast8unsigned"
| Ocast16signed -> "cast16signed"
| Ocast16unsigned -> "cast16unsigned"
| Osub -> "sub"
| 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)
| 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"
| Onegf -> "negf"
| Oabsf -> "absf"
| Oaddf -> "addf"
| Osubf -> "subf"
| Omulf -> "mulf"
| Odivf -> "divf"
| Osingleoffloat -> "singleoffloat"
| Ofloatofint -> "floatofint"
| Ocmp c -> Printf.sprintf "cmpcmpcmp"
| Olea _ -> "lea"
let to_coq_list = function
| [] -> []
| e :: l -> e :: l
let to_caml_list = function
| [] -> []
| e :: l -> e :: l
|
