docs/proof/RTLPar.html


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

<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<title>RTLPar.v</title>
<link rel="stylesheet" href="alectryon.css" type="text/css" />
<link rel="stylesheet" href="docutils_basic.css" type="text/css" />
<link rel="stylesheet" href="tango_subtle.css" type="text/css" />
<link rel="stylesheet" href="tango_subtle.min.css" type="text/css" />
<script type="text/javascript" src="alectryon.js"></script>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" />
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" />
</head>
<body>
<div class="alectryon-root alectryon-floating"><div class="document">


<pre class="alectryon-io"><!-- Generator: Alectryon v1.0 --><span class="coq-wsp"><span class="highlight"><span class="c">(*</span>
<span class="c"> * Vericert: Verified high-level synthesis.</span>
<span class="c"> * Copyright (C) 2020 Yann Herklotz &lt;yann@yannherklotz.com&gt;</span>
<span class="c"> *</span>
<span class="c"> * This program is free software: you can redistribute it and/or modify</span>
<span class="c"> * it under the terms of the GNU General Public License as published by</span>
<span class="c"> * the Free Software Foundation, either version 3 of the License, or</span>
<span class="c"> * (at your option) any later version.</span>
<span class="c"> *</span>
<span class="c"> * This program is distributed in the hope that it will be useful,</span>
<span class="c"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</span>
<span class="c"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the</span>
<span class="c"> * GNU General Public License for more details.</span>
<span class="c"> *</span>
<span class="c"> * You should have received a copy of the GNU General Public License</span>
<span class="c"> * along with this program.  If not, see &lt;https://www.gnu.org/licenses/&gt;.</span>
<span class="c"> *)</span>

</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Import</span> Coqlib Maps.</span></span><span class="coq-wsp">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Import</span> AST Integers Values Events Memory Globalenvs Smallstep.</span></span><span class="coq-wsp">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> compcert <span class="kn">Require Import</span> Op Registers.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">node</span> := positive.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">instruction</span> : <span class="kt">Type</span> :=
| RPnop : instruction
| RPop : operation -&gt; list reg -&gt; reg -&gt; instruction
| RPload : memory_chunk -&gt; addressing -&gt; list reg -&gt; reg -&gt; instruction
| RPstore : memory_chunk -&gt; addressing -&gt; list reg -&gt; reg -&gt; instruction.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">bblock_body</span> : <span class="kt">Type</span> := list (list instruction).</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Inductive</span> <span class="nf">control_flow_inst</span> : <span class="kt">Type</span> :=
| RPcall : signature -&gt; reg + <span class="kn">ident</span> -&gt; list reg -&gt; reg -&gt; node -&gt; control_flow_inst
| RPtailcall : signature -&gt; reg + <span class="kn">ident</span> -&gt; list reg -&gt; control_flow_inst
| RPbuiltin : external_function -&gt; list (builtin_arg reg) -&gt;
              builtin_res reg -&gt; node -&gt; control_flow_inst
| RPcond : condition -&gt; list reg -&gt; node -&gt; node -&gt; control_flow_inst
| RPjumptable : reg -&gt; list node -&gt; control_flow_inst
| RPreturn : option reg -&gt; control_flow_inst
| RPgoto : node -&gt; control_flow_inst.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Record</span> <span class="nf">bblock</span> : <span class="kt">Type</span> := mk_bblock {
    bb_body: bblock_body;
    bb_exit: option control_flow_inst
  }.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">code</span> : <span class="kt">Type</span> := PTree.t bblock.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Record</span> <span class="nf">function</span>: <span class="kt">Type</span> := mkfunction {
  fn_sig: signature;
  fn_params: list reg;
  fn_stacksize: Z;
  fn_code: code;
  fn_entrypoint: node
}.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">fundef</span> := AST.fundef function.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">program</span> := AST.program fundef unit.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">funsig</span> (<span class="nv">fd</span>: fundef) :=
  <span class="kr">match</span> fd <span class="kr">with</span>
  | Internal f =&gt; fn_sig f
  | External ef =&gt; ef_sig ef
  <span class="kr">end</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">successors_instr</span> (<span class="nv">i</span> : control_flow_inst) : list node :=
  <span class="kr">match</span> i <span class="kr">with</span>
  | RPcall sig ros args res s =&gt; s :: nil
  | RPtailcall sig ros args =&gt; nil
  | RPbuiltin ef args res s =&gt; s :: nil
  | RPcond cond args ifso ifnot =&gt; ifso :: ifnot :: nil
  | RPjumptable arg tbl =&gt; tbl
  | RPreturn optarg =&gt; nil
  | RPgoto n =&gt; n :: nil
  <span class="kr">end</span>.</span></span><span class="coq-wsp">
</span></span><span class="coq-wsp"><span class="highlight">
<span class="c">(*Inductive state : Type :=</span>
<span class="c">  | State:</span>
<span class="c">      forall (stack: list stackframe) (**r call stack *)</span>
<span class="c">             (f: function)            (**r current function *)</span>
<span class="c">             (sp: val)                (**r stack pointer *)</span>
<span class="c">             (pc: node)               (**r current program point in [c] *)</span>
<span class="c">             (rs: regset)             (**r register state *)</span>
<span class="c">             (m: mem),                (**r memory state *)</span>
<span class="c">      state</span>
<span class="c">  | Callstate:</span>
<span class="c">      forall (stack: list stackframe) (**r call stack *)</span>
<span class="c">             (f: fundef)              (**r function to call *)</span>
<span class="c">             (args: list val)         (**r arguments to the call *)</span>
<span class="c">             (m: mem),                (**r memory state *)</span>
<span class="c">      state</span>
<span class="c">  | Returnstate:</span>
<span class="c">      forall (stack: list stackframe) (**r call stack *)</span>
<span class="c">             (v: val)                 (**r return value for the call *)</span>
<span class="c">             (m: mem),                (**r memory state *)</span>
<span class="c">      state.</span>
<span class="c">*)</span></span></span></pre>
</div>
</div></body>
</html>