From 89f6064f6b0a1b5a6ba5e515ce38d7cf4ff37d22 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 1 May 2019 16:27:45 +0100
Subject: 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.
---
 language/jib.ott | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

(limited to 'language')

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
-- 
cgit v1.2.3