diff options
| author | Alasdair Armstrong | 2019-04-09 18:30:37 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-09 20:35:50 +0100 |
| commit | 271a8aba3041e4f712f3331fd1610cdf31fbb4c9 (patch) | |
| tree | 1644d1916b76e8e75606a63cf3d92b71358b26de /language | |
| parent | 97cc026337ea5cfc33586b6725c312c1a507f922 (diff) | |
SMT: Refactor Jib values to make inlining work
Had to change the hundreds and hundreds of places such values were
used. However this now lets us automatically prove cheri-concentrate
properties. Such as showing
function prop_cap_round_trip(cap: bits(128)) -> bool = {
let cap_rt = capToBits(capBitsToCapability(true, cap));
cap == cap_rt
}
is always true.
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/language/jib.ott b/language/jib.ott index d7a8b188..8177ae3a 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -41,6 +41,10 @@ metavar value ::= {{ lem vl }} {{ ocaml vl }} +metavar alpha ::= + {{ phantom }} + {{ lem 'a }} + embed {{ lem @@ -60,19 +64,20 @@ name :: '' ::= % Fragments are small pure snippets of (abstract) C code, mostly % expressions, used by the aval (ANF) and cval (Jib) types. -fragment :: 'F_' ::= - | name :: :: id - | '&' name :: :: ref - | value :: :: lit - | fragment != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind - | unwrap id ( ctyp0 , ... , ctypn ) fragment :: :: ctor_unwrap - | fragment op fragment' :: :: op - | fragment nat0 nat1 :: :: tuple_member - | op fragment :: :: unary - | string ( fragment0 , ... , fragmentn ) :: :: call - | fragment . string :: :: field - | string :: :: raw - | poly fragment :: :: poly +cval :: 'V_' ::= + | name : ctyp :: :: id + | '&' name : ctyp :: :: ref + | value : ctyp :: :: lit + | cval != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind + | unwrap id cval ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_unwrap + | cval op cval' :: :: op + | cval nat0 nat1 :: :: tuple_member + | op cval :: :: unary + | string ( cval0 , ... , cvaln ) :: :: call + | cval . string :: :: field + | hd ( cval ) :: :: hd + | tl ( cval ) :: :: tl + | poly cval ctyp :: :: poly % Note that init / clear are sometimes refered to as create / kill @@ -135,11 +140,6 @@ ctyp :: 'CT_' ::= % lbits, and this must work without compiling to type incorrect C. | poly :: :: poly - -cval :: 'CV_' ::= - {{ ocaml fragment * ctyp }} - {{ lem fragment * ctyp }} - clexp :: 'CL_' ::= | name : ctyp :: :: id | name0 rmw name1 : ctyp :: :: rmw |