Skip to content

Ite predication #9

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ivg merged 2 commits into from
Aug 8, 2018
Merged

Ite predication #9

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
dffddbc
Revert "Commit on wrong branch."
Jul 25, 2018
c273308
Change ite syntax
Jul 25, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 18 additions & 6 deletions bil.ott
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ grammar
{{ com -- bind $e_1$ to $var$ in expression $e_2$}}
| unknown [ string ] : type :: :: unk
{{ com -- unknown or undefined value of a given $type$ }}
| if e1 then e2 else e3 :: :: ite
| ite e1 e2 e3 :: :: ite
{{ com -- evaluates to $e_2$ if $e_1$ is true else to $e_3$ }}
| extract : nat1 : nat2 [ e ] :: :: ext
{{ com -- extract or extend bitvector $e$}}
Expand Down Expand Up @@ -384,7 +384,7 @@ defns typing_exp :: '' ::=
G |- e2 :: t
G |- e3 :: t
-------------------------- :: ite
G |- if e1 then e2 else e3 :: t
G |- ite e1 e2 e3 :: t

G |- e :: imm<sz>
sz1 >= sz2
Expand Down Expand Up @@ -580,15 +580,27 @@ defns reduce_exp :: '' ::=


delta |- e1 ~> e1'
------------------------------------------------------------------ :: ite_step
delta |- if e1 then e2 else e3 ~> if e1' then e2 else e3
------------------------------------------------------------------ :: ite_step_cond
delta |- ite e1 v2 v3 ~> ite e1' v2 v3

delta |- e2 ~> e2'
------------------------------------------------------------------ :: ite_step_then
delta |- ite e1 e2 v3 ~> ite e1 e2' v3

delta |- e3 ~> e3'
------------------------------------------------------------------ :: ite_step_else
delta |- ite e1 e2 e3 ~> ite e1 e2 e3'

----------------------------------------------- :: ite_true
delta |- if true then e2 else e3 ~> e2
delta |- ite true v2 v3 ~> v2


------------------------------------------------ :: ite_false
delta |- if false then e2 else e3 ~> e3
delta |- ite false v2 v3 ~> v3

type(v2) = t'
------------------------------------------------------------------ :: ite_unk
delta |- ite unknown[str]:t v2 v3 ~> unknown[str]:t'

delta |- e2 ~> e2'
------------------------------------------ :: bop_rhs
Expand Down