Skip to content
Snippets Groups Projects
Commit fbd43abe authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'interpreter' into 'master' 

Add a verified interpreter for HeapLang

See merge request iris/iris!564
parents d3e1e7ff e5f526c3
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 3
− 0
View file @ fbd43abe
......@@ -142,6 +142,7 @@ iris/proofmode/modality_instances.v
iris_heap_lang/locations.v
iris_heap_lang/lang.v
iris_heap_lang/class_instances.v
iris_heap_lang/pretty.v
iris_heap_lang/metatheory.v
iris_heap_lang/tactics.v
iris_heap_lang/primitive_laws.v
......@@ -174,3 +175,5 @@ iris_deprecated/base_logic/auth.v
iris_deprecated/base_logic/sts.v
iris_deprecated/base_logic/viewshifts.v
iris_deprecated/program_logic/hoare.v
iris_staging/heap_lang/interpreter.v
coq-iris-staging.opam
+ 1
− 0
View file @ fbd43abe
......@@ -14,6 +14,7 @@ work is needed before they are ready for this.
depends: [
"coq-iris" {= version}
"coq-iris-heap-lang" {= version}
]
build: ["./make-package" "iris_staging" "-j%{jobs}%"]
......
iris_heap_lang/locations.v
+ 5
− 3
View file @ fbd43abe
......@@ -2,15 +2,17 @@ From stdpp Require Import countable numbers gmap.
From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
Record loc := { loc_car : Z }.
Record loc := Loc { loc_car : Z }.
Add Printing Constructor loc.
Global Instance loc_eq_decision : EqDecision loc.
Proof. solve_decision. Qed.
Proof. solve_decision. Defined.
Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
Global Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' loc_car (λ i, {| loc_car := i |})); intros []. Qed.
Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
......
iris_heap_lang/pretty.v 0 → 100644
+ 65
− 0
View file @ fbd43abe
From stdpp Require Export pretty.
From iris.heap_lang Require Import lang.
From iris.prelude Require Import options.
(** * Pretty printing for HeapLang values *)
Global Instance pretty_loc : Pretty loc :=
λ l, pretty l.(loc_car).
Global Instance pretty_base_lit : Pretty base_lit :=
λ l, match l with
| LitInt z => pretty z
| LitBool b => if b then "true" else "false"
| LitUnit => "()"
| LitPoison => "<poison>"
| LitLoc l => "(loc " +:+ pretty l +:+ ")"
| LitProphecy i => "(prophecy " +:+ pretty i +:+ ")"
end.
Global Instance pretty_binder : Pretty binder :=
λ b, match b with
| BNamed x => x
| BAnon => "<>"
end.
(** Note that this instance does not print function bodies and is thus not
injective (unlike most `pretty` instances). *)
Global Instance pretty_val : Pretty val :=
fix go v :=
match v with
| LitV l => "#" +:+ pretty l
| RecV f x e =>
match f with
| BNamed f => "rec: " +:+ f +:+ " " +:+ pretty x +:+ " := <body>"
| BAnon => "λ: " +:+ pretty x +:+ ", <body>"
end
| PairV v1 v2 => "(" +:+ go v1 +:+ ", " +:+ go v2 +:+ ")"
| InjLV v => "inl (" +:+ go v +:+ ")"
| InjRV v => "inr (" +:+ go v +:+ ")"
end.
Global Instance pretty_un_op : Pretty un_op :=
λ op, match op with
| NegOp => "~"
| MinusUnOp => "-"
end.
Global Instance pretty_bin_op : Pretty bin_op :=
λ op, match op with
| PlusOp => "+"
| MinusOp => "-"
| MultOp => "*"
| QuotOp => "`quot`"
| RemOp => "`rem`"
| AndOp => "&"
| OrOp => "|"
| XorOp => "`xor`"
| ShiftLOp => "<<"
| ShiftROp => ">>"
| LeOp => "≤"
| LtOp => "<"
| EqOp => "="
| OffsetOp => "+ₗ"
end .
iris_staging/heap_lang/interpreter.v 0 → 100644
+ 1004
− 0
View file @ fbd43abe
This diff is collapsed.
tests/heap_lang_interpreter.ref 0 → 100644
+ 44
− 0
View file @ fbd43abe
"ex1"
: string
= inl #()
: val + Error
"ex3"
: string
= inl #2
: val + Error
"ex4"
: string
= inl #(Loc 2)
: val + Error
"ex5"
: string
= inl #false
: val + Error
"ex6"
: string
= inl #2
: val + Error
"fail app non-function"
: string
= inr (Stuck "attempt to call non-function #2")
: val + Error
"fail loc order"
: string
= inr
(Stuck
"bin-op failed: the only supported operation on locations is +ₗ #i, got < #(loc 2)")
: val + Error
"fail compare pairs"
: string
= inr
(Stuck
"bin-op failed: one of (#0, #1) and (#0, #1) must be unboxed to compare: (#0, #1): pairs are large and considered boxed, must compare by field, (#0, #1): pairs are large and considered boxed, must compare by field")
: val + Error
"fail free var"
: string
= inr (Stuck "free var: x")
: val + Error
"fail out of fuel"
: string
= inl (rec: "foo" <> := "foo" #())%V
: val + Error
tests/heap_lang_interpreter.v 0 → 100644
+ 66
− 0
View file @ fbd43abe
From iris.heap_lang Require Import notation.
From iris.staging.heap_lang Require Import interpreter.
Example test_1 :
exec 1000 ((λ: "x", "x" + #1) #2) = inl #3.
Proof. reflexivity. Qed.
Check "ex1".
Eval vm_compute in
exec 1000 (let: "x" := ref #() in
let: "y" := ref #() in
!"y").
Check "ex3".
(** eval order *)
Eval vm_compute in
exec 1000 (let: "x" := ref #1 in
let: "y" := ref #2 in
("y" <- !"x",
(* this runs first, so the result is 2 *)
"x" <- !"y");;
!"x").
(* print a location *)
Check "ex4".
Eval vm_compute in
exec 1000 (ref #();; ref #()).
Check "ex5".
Eval vm_compute in
exec 1000 (let: "x" := ref #() in
let: "y" := ref #() in
"x" = "y").
(* a bad case where the interpreter runs a program which is actually stuck,
because this program guesses an allocation that happens to be correct in the
interpreter *)
Check "ex6".
Eval vm_compute in
exec 1000 (let: "x" := ref #1 in
#(LitLoc {|loc_car := 1|}) <- #2;;
!"x").
(** * Failing executions *)
Check "fail app non-function".
Eval vm_compute in
exec 1000 (#2 #4).
(* locations are not ordered *)
Check "fail loc order".
Eval vm_compute in
exec 1000 (let: "x" := ref #() in
let: "y" := ref #() in
"x" < "y").
Check "fail compare pairs".
Eval vm_compute in
exec 1000 ((#0, #1) = (#0, #1)).
Check "fail free var".
Eval vm_compute in exec 100 "x".
Check "fail out of fuel".
(** infinite loop *)
Eval vm_compute in exec 100 (rec: "foo" <> := "foo" #()).
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