diff options
| author | Alasdair Armstrong | 2019-04-05 14:45:21 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-04-09 16:16:32 +0100 |
| commit | 97cc026337ea5cfc33586b6725c312c1a507f922 (patch) | |
| tree | 93d9682e005855b58e8eec6cf6e649d22df1f5c3 /language | |
| parent | 76bf4a3853e547ae2e0327b20e4f4b89d16820b7 (diff) | |
SMT: Experimental Jib->SMT translation
Currently only works with CVC4, test cases are in test/smt. Can prove
that RISC-V add instruction actually adds values in registers and
that's about it for now.
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/language/jib.ott b/language/jib.ott index 5f800fcd..d7a8b188 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -7,6 +7,10 @@ metavar nat ::= {{ ocaml int }} {{ lem nat }} +metavar big_int ::= + {{ phantom }} + {{ lem integer }} + metavar id ::= {{ phantom }} {{ ocaml id }} @@ -63,6 +67,7 @@ fragment :: 'F_' ::= | 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 @@ -81,6 +86,7 @@ ctyp :: 'CT_' ::= % fint(n) is a fixed precision signed integer that is representable in exactly n bits | lint :: :: lint | fint nat :: :: fint + | constant big_int :: :: constant % Bitvector types - flag represents bit indexing direction, true - dec or false - inc % @@ -136,6 +142,7 @@ cval :: 'CV_' ::= clexp :: 'CL_' ::= | name : ctyp :: :: id + | name0 rmw name1 : ctyp :: :: rmw | clexp . string :: :: field | * clexp :: :: addr | clexp . nat :: :: tuple |