Skip to content

why3
why3
Commit e0a52cb1 authored by Jean-Christophe Filliatre's avatar Jean-Christophe Filliatre
Browse files
Options

new example: tiny register allocator for tree expressions (wip)

parent e10f46c2
Hide whitespace changes
Inline Side-by-side
Showing with 304 additions and 0 deletions
examples/register_allocation.mlw 0 → 100644
View file @ e0a52cb1
(** A tiny register allocator for tree expressions. *)
module Spec
use import HighOrd
use import int.Int
type addr
type expr =
| Evar addr
| Eneg expr
| Eadd expr expr
type memory = addr -> int
function eval (m: memory) (e: expr) : int =
match e with
| Evar x -> m x
| Eneg e -> - (eval m e)
| Eadd e1 e2 -> eval m e1 + eval m e2
end
type register = int
type instr =
| Iload addr register
| Ineg register
| Iadd register register
| Ipush register
| Ipop register
type registers = register -> int
function update (reg: registers) (r: register) (v: int) : registers =
\r'. if r' = r then v else reg r'
use import list.List
type stack = list int
type state = {
mem: memory;
reg: registers;
st : stack;
}
function exec (i: instr) (s: state) : state =
match i with
| Iload x r -> { s with reg = update s.reg r (s.mem x) }
| Ineg r -> { s with reg = update s.reg r (- s.reg r) }
| Iadd r1 r2 -> { s with reg = update s.reg r2 (s.reg r1 + s.reg r2) }
| Ipush r -> { s with st = Cons (s.reg r) s.st }
| Ipop r -> match s.st with
| Nil -> s (* fails *)
| Cons v st -> { s with reg = update s.reg r v; st = st }
end
end
type code = list instr
function exec_list (c: code) (s: state) : state =
match c with
| Nil -> s
| Cons i l -> exec_list l (exec i s)
end
use import list.Append
let rec lemma exec_append (c1 c2: code) (s: state) : unit
ensures { exec_list (c1 ++ c2) s = exec_list c2 (exec_list c1 s) }
variant { c1 }
= match c1 with
| Nil -> ()
| Cons i1 l1 -> exec_append l1 c2 (exec i1 s)
end
end
module InfinityOfRegisters
use import HighOrd
use import int.Int
use import list.List
use import list.Append
use import Spec
(** [compile e r] returns a list of instructions that stores the value
of [e] in register [r], without modifying any register [r' < r]. *)
let rec compile (e: expr) (r: register) : code
variant { e }
ensures { forall s. let s' = exec_list result s in
s'.mem = s.mem /\
s'.reg r = eval s.mem e /\
forall r'. r' < r -> s'.reg r' = s.reg r' }
=
match e with
| Evar x ->
Cons (Iload x r) Nil
| Eneg e ->
compile e r ++ Cons (Ineg r) Nil
| Eadd e1 e2 ->
compile e1 r ++ compile e2 (r + 1) ++ Cons (Iadd (r + 1) r) Nil
end
end
module FiniteNumberOfRegisters
use import HighOrd
use import int.Int
use import list.List
use import list.Append
use import Spec
(** we have k registers, namely 0,1,...,k-1 *)
constant k: int
(** we assume having at least two registers, otherwise we can't add *)
axiom at_least_two_registers: k >= 2
(** [compile e r] returns a list of instructions that stores the value
of [e] in register [r], without modifying any register [r' < r]. *)
(** PROOF TO BE COMPLETED
let rec compile (e: expr) (r: register) : code
requires { 0 <= r < k }
variant { e }
ensures { forall s. let s' = exec_list result s in
s'.mem = s.mem /\
s'.st = s.st /\
s'.reg r = eval s.mem e /\
forall r'. r' < r -> s'.reg r' = s.reg r' }
=
match e with
| Evar x ->
Cons (Iload x r) Nil
| Eneg e ->
compile e r ++ Cons (Ineg r) Nil
| Eadd e1 e2 ->
if r < k-1 then
compile e1 r ++ compile e2 (r + 1) ++ Cons (Iadd (r + 1) r) Nil
else
Cons (Ipush (k - 2)) (
compile e1 (k - 2) ++ compile e2 (k - 1) ++
Cons (Iadd (k - 2) (k - 1)) (
Cons (Ipop (k - 2)) Nil))
end
**)
end
examples/register_allocation/why3session.xml 0 → 100644
View file @ e0a52cb1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="2" name="Spass" version="3.7" timelimit="61" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.0" timelimit="61" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="61" memlimit="1000"/>
<file name="../register_allocation.mlw" expanded="true">
<theory name="Spec" sum="f1ac77bc98c04a42c874b237366bfbc8">
<goal name="WP_parameter exec_append" expl="VC for exec_append">
<proof prover="0" steplimit="1"><result status="valid" time="0.03" steps="89"/></proof>
</goal>
</theory>
<theory name="InfinityOfRegisters" sum="aca0ffe746fe1c272a24095f886f08d2">
<goal name="WP_parameter compile" expl="VC for compile">
<transf name="split_goal_wp">
<goal name="WP_parameter compile.1" expl="1. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter compile.1.1" expl="1. postcondition">
<proof prover="0" steplimit="1"><result status="valid" time="0.02" steps="43"/></proof>
</goal>
<goal name="WP_parameter compile.1.2" expl="2. postcondition">
<proof prover="0" steplimit="1"><result status="valid" time="0.02" steps="77"/></proof>
<proof prover="1" steplimit="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter compile.1.3" expl="3. postcondition">
<proof prover="0" steplimit="1"><result status="valid" time="0.01" steps="76"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter compile.2" expl="2. variant decrease">
<proof prover="0" steplimit="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter compile.3" expl="3. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter compile.3.1" expl="1. postcondition">
<proof prover="0" steplimit="1"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="WP_parameter compile.3.2" expl="2. postcondition">
<proof prover="1" steplimit="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter compile.3.3" expl="3. postcondition">
<proof prover="0" steplimit="1"><result status="valid" time="0.06" steps="92"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter compile.4" expl="4. variant decrease">
<proof prover="0" steplimit="1"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter compile.5" expl="5. variant decrease">
<proof prover="0" steplimit="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter compile.6" expl="6. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter compile.6.1" expl="1. postcondition">
<proof prover="1" steplimit="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter compile.6.2" expl="2. postcondition">
<proof prover="1" steplimit="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter compile.6.3" expl="3. postcondition">
<proof prover="1" steplimit="1"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
<theory name="FiniteNumberOfRegisters" sum="0f4a5f62bcb1053f688e2787726e5867" expanded="true">
<goal name="WP_parameter compile" expl="VC for compile" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter compile.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.12" steps="202"/></proof>
</goal>
<goal name="WP_parameter compile.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter compile.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter compile.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.16" steps="238"/></proof>
</goal>
<goal name="WP_parameter compile.5" expl="5. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter compile.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter compile.7" expl="7. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="WP_parameter compile.8" expl="8. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter compile.9" expl="9. postcondition">
<proof prover="1"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="WP_parameter compile.10" expl="10. variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter compile.11" expl="11. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter compile.12" expl="12. variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter compile.13" expl="13. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter compile.14" expl="14. postcondition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter compile.14.1" expl="1. postcondition">
<proof prover="0" timelimit="61"><result status="timeout" time="5.98"/></proof>
<proof prover="1" timelimit="61"><result status="timeout" time="6.01"/></proof>
<proof prover="2"><result status="timeout" time="61.77"/></proof>
<proof prover="3"><result status="timeout" time="60.85"/></proof>
<proof prover="4"><result status="outofmemory" time="40.90"/></proof>
</goal>
<goal name="WP_parameter compile.14.2" expl="2. postcondition">
<proof prover="0" timelimit="61"><result status="timeout" time="5.98"/></proof>
<proof prover="1" timelimit="61"><result status="timeout" time="6.02"/></proof>
<proof prover="2"><result status="timeout" time="61.81"/></proof>
<proof prover="3"><result status="timeout" time="60.84"/></proof>
<proof prover="4"><result status="outofmemory" time="40.66"/></proof>
</goal>
<goal name="WP_parameter compile.14.3" expl="3. postcondition">
<proof prover="0" timelimit="61"><result status="timeout" time="5.98"/></proof>
<proof prover="1" timelimit="61"><result status="timeout" time="6.00"/></proof>
<proof prover="2"><result status="timeout" time="6.45"/></proof>
<proof prover="3"><result status="timeout" time="60.86"/></proof>
<proof prover="4"><result status="outofmemory" time="36.41"/></proof>
</goal>
<goal name="WP_parameter compile.14.4" expl="4. postcondition">
<proof prover="0" timelimit="61"><result status="timeout" time="5.99"/></proof>
<proof prover="1" timelimit="61"><result status="timeout" time="6.05"/></proof>
<proof prover="2"><result status="timeout" time="6.03"/></proof>
<proof prover="3"><result status="timeout" time="60.87"/></proof>
<proof prover="4"><result status="outofmemory" time="40.84"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment