From 47b635a18292be4c805145fb7f45ebbc670aa240 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@cl.cam.ac.uk>
Date: Thu, 24 Aug 2023 13:47:05 +0100
Subject: [PATCH] CN: CLogicalFuns: support yet more syntax

Continue expanding the collection of Mucore syntax forms that CLogicalFuns
can map to CN syntax. It should probably be explained that this work began
with bd167f87a (two commits ago) which was pushed with no commit message by
mistake, whose main change was to refactor the mucore->index-term conversion
to handle if-then-else splits.
---
 backend/cn/cLogicalFuns.ml | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/backend/cn/cLogicalFuns.ml b/backend/cn/cLogicalFuns.ml
index 0ea9ca0fe..a03d8f51d 100644
--- a/backend/cn/cLogicalFuns.ml
+++ b/backend/cn/cLogicalFuns.ml
@@ -20,6 +20,7 @@ let mu_val_to_it = function
   | M_Vtrue -> Some (IT.bool_ true)
   | M_Vfalse -> Some (IT.bool_ false)
   | M_Vobject (M_OVinteger iv) -> Some (IT.z_ (Memory.z_of_ival iv))
+  | M_Vctype ct -> Option.map IT.const_ctype_ (Sctypes.of_ctype ct)
   | _ -> None
 
 let local_sym_ptr = Sym.fresh_named "local_ptr"
@@ -52,6 +53,12 @@ let upd_loc_state state ix v =
   let loc_map = IntMap.add ix (Some v) state.loc_map in
   { state with loc_map }
 
+let do_wrapI loc ct it =
+  match Sctypes.is_integer_type ct with
+  | Some ity -> return (IT.wrapI_ (ity, it))
+  | None -> fail {loc; msg = Generic (Pp.item "expr from C syntax: coercion to non-int type"
+      (Sctypes.pp ct))}
+
 let rec symb_exec_mu_pexpr var_map pexpr =
   let (M_Pexpr (loc, _, _, pe)) = pexpr in
   match pe with
@@ -70,6 +77,8 @@ let rec symb_exec_mu_pexpr var_map pexpr =
     begin match op with
     | OpAdd -> return (IT.add_ (x_v, y_v))
     | OpSub -> return (IT.sub_ (x_v, y_v))
+    | OpMul -> return (IT.mul_ (x_v, y_v))
+    | OpDiv -> return (IT.div_ (x_v, y_v))
     | OpEq  -> return (IT.eq_ (x_v, y_v))
     | OpLt  -> return (IT.lt_ (x_v, y_v))
     | OpLe  -> return (IT.le_ (x_v, y_v))
@@ -82,8 +91,18 @@ let rec symb_exec_mu_pexpr var_map pexpr =
     end
   | M_PEconv_int (ct_expr, pe)
   | M_PEconv_loaded_int (ct_expr, pe) ->
-    (* FIXME revisit this, just ignoring wrapping here *)
-    symb_exec_mu_pexpr var_map pe
+    let@ x = symb_exec_mu_pexpr var_map pe in
+    let@ ct_it = symb_exec_mu_pexpr var_map ct_expr in
+    let@ ct = match IT.is_const ct_it with
+    | Some (IT.CType_const ct, _) -> return ct
+    | Some _ -> assert false (* shouldn't be possible given type *)
+    | None -> fail {loc; msg = Generic (Pp.item "expr from C syntax: non-constant type"
+        (IT.pp ct_it))}
+    in
+    do_wrapI loc ct x
+  | M_PEwrapI (act, pe) ->
+    let@ x = symb_exec_mu_pexpr var_map pe in
+    do_wrapI loc act.ct x
   | _ -> fail {loc; msg = Generic (Pp.item "getting expr from C syntax: unsupported pure expr"
         (Pp_mucore.pp_pexpr pexpr))}