Fix #122 by using operators that are consistent with the type of the operands

lib/AstOfLlbc.ml

@@ -650,9 +650,12 @@ let expression_of_place (env : env) (p : C.place) : K.expr =
   L.log "AstOfLlbc" "expression of place: %s" (C.show_place p);
   expression_of_place env p
 
+(* We produce bit-wise operators first, then when the type is of booleans, we
+   change into the non-B variants (Rust does not distinguish between bitwise and
+   boolean operators) *)
 let op_of_unop (op : C.unop) : Krml.Constant.op =
   match op with
-  | C.Not -> Not
+  | C.Not -> BNot
   | C.Neg -> Neg
   | _ -> assert false
 
@@ -684,8 +687,13 @@ let mk_op_app (op : K.op) (first : K.expr) (rest : K.expr list) : K.expr =
     | t -> fail "Not an operator type: %a" ptyp t
   in
   let op =
-    if op = Not && first.typ <> K.TBool then
-      Krml.Constant.BNot
+    if first.typ = K.TBool then
+      match op with
+      | BNot -> Krml.Constant.Not
+      | BAnd -> And
+      | BOr -> Or
+      | BXor -> Xor
+      | op -> op
     else
       op
   in
@@ -1764,7 +1772,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =
               (fun ({ C.variant_name; discriminant; _ } : C.variant) ->
                 let v =
                   if has_custom_constants then
-                    Some (Z.to_int discriminant.value)
+                    Some discriminant.value
                   else
                     None
                 in

lib/Bundles.ml

@@ -458,27 +458,28 @@ let reassign_monomorphizations (files : Krml.Ast.file list) (config : config) =
     Krml.MonomorphizationState.generated_lids;
   (* Review the type monomorphization state. *)
   Hashtbl.iter
-    (fun (generic_lid, ts, _) (_, monomorphized_lid) ->
+    (fun (generic_lid, ts, _) (_, monomorphized_lid, normalized) ->
       (* Krml.KPrint.bprintf "generic=%a, monomorphized=%a\n" plid generic_lid plid monomorphized_lid; *)
-      match
-        List.find_map
-          (fun {
-                 name;
-                 inline_static;
-                 monomorphizations_of;
-                 monomorphizations_using;
-                 monomorphizations_exact;
-                 _;
-               } ->
-            find_map (matches monomorphized_lid) monomorphizations_exact
-            ||| List.find_map (uses monomorphizations_using) ts
-            ||| find_map (matches generic_lid) monomorphizations_of
-            |> Option.map (fun vis -> name, inline_static, vis))
-          config
-      with
-      | Some name -> Hashtbl.add target_of_lid monomorphized_lid name
-      | None -> ())
-    Krml.Monomorphization.state;
+      if not normalized then
+        match
+          List.find_map
+            (fun {
+                   name;
+                   inline_static;
+                   monomorphizations_of;
+                   monomorphizations_using;
+                   monomorphizations_exact;
+                   _;
+                 } ->
+              find_map (matches monomorphized_lid) monomorphizations_exact
+              ||| List.find_map (uses monomorphizations_using) ts
+              ||| find_map (matches generic_lid) monomorphizations_of
+              |> Option.map (fun vis -> name, inline_static, vis))
+            config
+        with
+        | Some name -> Hashtbl.add target_of_lid monomorphized_lid name
+        | None -> ())
+    Krml.MonomorphizationState.state;
   (* Debug *)
   Hashtbl.iter
     (fun lid (target, _inline_static, vis) ->

test/issue_123/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "issue_123"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

test/issue_123/src/main.rs

@@ -0,0 +1,39 @@
+enum Gamma2 {
+    V95_232 = 95_232,
+    V261_888 = 261_888,
+}
+
+enum E1 {
+    C1 = 0xffffffff,
+    C2 = -0xffffffff,
+    C3 = 0x0fffffff
+}
+
+#[derive(PartialEq)]
+enum E2 {
+    C1 = 0xff,
+    C2 = -1,
+}
+
+enum E3 {
+    C1 = 0xff
+}
+
+enum E4 {
+    C1 = 0x7f,
+    C2 = -0x7e
+}
+
+enum E {
+    One = 1,
+    Five = 5,
+}
+
+fn fun(e: E) -> i32 {
+    e as i32
+}
+
+fn main() {
+    assert_eq!(E2::C1 as isize, -1);
+    assert_eq!(fun(E::One), 1);
+}