From ec8cad1daa76fb265014d3d313173905925c9922 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 13 Mar 2019 14:26:59 +0000
Subject: C: Improve Jib IR, add SSA representation

Add a CL_void l-expression so we don't have redundant unit-typed
variables everywhere, and add an optimization in Jib_optimize called
optimize_unit which introduces these.

Remove the basic control-flow graph in Jib_util and add a new mutable
control-flow graph type in Jib_ssa which allows the IR to be converted
into SSA form. The mutable graph allows for more efficient updates,
and includes both back and forwards references making it much more
convenient to traverse.

Having an SSA representation should make some optimizations much
simpler, and is also probably more natural for SMT generation where
variables have to be defined once using declare-const anyway.

Debug option -ddump_flow_graphs now outputs SSA'd graphs of the
functions in a specification.
---
 language/jib.ott | 1 +
 1 file changed, 1 insertion(+)

(limited to 'language')

diff --git a/language/jib.ott b/language/jib.ott
index 7b5d0162..e54e2ea5 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -136,6 +136,7 @@ clexp :: 'CL_' ::=
   | current_exception : ctyp :: :: current_exception
   | have_exception           :: :: have_exception
   | return : ctyp            :: :: return
+  | void                     :: :: void
 
 ctype_def :: 'CTD_' ::=
   {{ com C type definition }}
-- 
cgit v1.2.3