diff options
| author | Alasdair Armstrong | 2019-05-01 16:27:45 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-01 16:32:28 +0100 |
| commit | 89f6064f6b0a1b5a6ba5e515ce38d7cf4ff37d22 (patch) | |
| tree | c5dacad57a9e44f53c876eac84bffcdd55d91894 /language | |
| parent | 58d46e240315abb684823812ff1b2a9684653e5d (diff) | |
Jib: Refactor V_call
Get rid of separate V_op and V_unary constructors. jib.ott now defines
the valid operations for V_call including zero/sign extension, in such
a way that the operation ctyp can be inferred. Overall this makes the
IR less ad-hoc, and means we can share more code between SMT and C.
string_of_cval no longer used by c_backend, which now uses sgen_cval
following other sgen_ functions in the code generator, meaning
string_of_cval doesn't have to produce valid C code anymore and so can
be used for backend-agnostic debug and error messages.
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 32 |
1 files changed, 20 insertions, 12 deletions
diff --git a/language/jib.ott b/language/jib.ott index f0fdde2b..558c4db7 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -26,11 +26,6 @@ metavar string ::= {{ ocaml string }} {{ lem string }} -metavar op ::= - {{ phantom }} - {{ ocaml string }} - {{ lem string }} - metavar bool ::= {{ phantom }} {{ ocaml bool }} @@ -61,8 +56,25 @@ name :: '' ::= | current_exception nat :: :: current_exception | return nat :: :: return -% Fragments are small pure snippets of (abstract) C code, mostly -% expressions, used by the aval (ANF) and cval (Jib) types. +op :: '' ::= + | not :: :: bnot + | hd :: :: list_hd + | tl :: :: list_tl + | bit_to_bool :: :: bit_to_bool + | eq :: :: eq + | neq :: :: neq +% Integer ops + | lt :: :: ilt + | lteq :: :: ilteq + | gt :: :: igt + | gteq :: :: igteq + | add :: :: iadd + | sub :: :: isub +% Bitvector ops + | bvor :: :: bvor + | bvand :: :: bvand + | zero_extend nat :: :: zero_extend + | sign_extend nat :: :: sign_extend cval :: 'V_' ::= | name : ctyp :: :: id @@ -71,13 +83,9 @@ cval :: 'V_' ::= | struct { id0 = cval0 , ... , idn = cvaln } ctyp :: :: struct | 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 + | op ( 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 |