diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-20 14:53:34 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-20 14:53:34 +0000 |
| commit | 8588ebb4621d85b7ccc738622339b3aa53486c31 (patch) | |
| tree | 89e78e3ec67f884f7062aebb81b68aa54cf5fc1c /docs/proof/RTLPar.html | |
| parent | 34afd2f6ea0fc55cca1c674ab9b2f181be878291 (diff) | |
| download | vericert-8588ebb4621d85b7ccc738622339b3aa53486c31.tar.gz vericert-8588ebb4621d85b7ccc738622339b3aa53486c31.zip | |
Delete documents folder and move to separate repository
Diffstat (limited to 'docs/proof/RTLPar.html')
| -rw-r--r-- | docs/proof/RTLPar.html | 121 |
1 files changed, 0 insertions, 121 deletions
diff --git a/docs/proof/RTLPar.html b/docs/proof/RTLPar.html deleted file mode 100644 index 461c9f0..0000000 --- a/docs/proof/RTLPar.html +++ /dev/null @@ -1,121 +0,0 @@ -<?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 <yann@yannherklotz.com></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 <https://www.gnu.org/licenses/>.</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 -> list reg -> reg -> instruction -| RPload : memory_chunk -> addressing -> list reg -> reg -> instruction -| RPstore : memory_chunk -> addressing -> list reg -> reg -> 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 -> reg + <span class="kn">ident</span> -> list reg -> reg -> node -> control_flow_inst -| RPtailcall : signature -> reg + <span class="kn">ident</span> -> list reg -> control_flow_inst -| RPbuiltin : external_function -> list (builtin_arg reg) -> - builtin_res reg -> node -> control_flow_inst -| RPcond : condition -> list reg -> node -> node -> control_flow_inst -| RPjumptable : reg -> list node -> control_flow_inst -| RPreturn : option reg -> control_flow_inst -| RPgoto : node -> 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 => fn_sig f - | External ef => 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 => s :: nil - | RPtailcall sig ros args => nil - | RPbuiltin ef args res s => s :: nil - | RPcond cond args ifso ifnot => ifso :: ifnot :: nil - | RPjumptable arg tbl => tbl - | RPreturn optarg => nil - | RPgoto n => 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> |