CN: Add support for bitwise and in spec

An initial version of this commit had an incorrect type annotation in
`BW_And` in `compile.ml`; it was inconsequential because it is never
read/immediately written over by `Welltyped.infer`.

backend/cn/compile.ml

@@ -453,6 +453,8 @@ module EffectfulTranslation = struct
     fail { loc; msg = Generic msg }
 
 
+  (* TODO: type checks and disambiguation at this stage seems ill-advised,
+     ideally would be integrated into wellTyped.ml *)
   let mk_translate_binop loc' bop (e1, e2) =
     let open IndexTerms in
     let loc = loc' in
@@ -534,24 +536,8 @@ module EffectfulTranslation = struct
             }
       in
       return (IT (MapGet (e1, e2), rbt, loc))
-    | _ ->
-      let open Pp in
-      let msg =
-        !^"Ill-typed application of binary operation"
-        ^^^ squotes (CF.Cn_ocaml.PpAil.pp_cn_binop bop)
-        ^^^ dot
-        ^/^ !^"Left-hand-side:"
-        ^^^ squotes (IT.pp e1)
-        ^^^ !^"of type"
-        ^^^ squotes (SBT.pp (IT.bt e1))
-        ^^ comma
-        ^/^ !^"right-hand-side:"
-        ^^^ squotes (IT.pp e2)
-        ^^^ !^"of type"
-        ^^^ squotes (SBT.pp (IT.bt e2))
-        ^^ dot
-      in
-      fail { loc; msg = Generic msg }
+    | CN_band, (SBT.Bits _ as bt) -> return (IT (Binop (BW_And, e1, e2), bt, loc))
+    | _ -> fail { loc; msg = Illtyped_binary_it { left = e1; right = e2; binop = bop } }
 
 
   (* just copy-pasting and adapting Kayvan's older version of this code *)

backend/cn/typeErrors.ml

@@ -156,18 +156,21 @@ type message =
       { has : document;
         expect : document
       }
-  | Illtyped_it :
+  | Illtyped_it of
       { it : Pp.document;
-        has : Pp.document;
+        has : Pp.document; (* 'expected' and 'has' as in Kayvan's Core type checker *)
         expected : string;
         reason : string
       }
-      -> message (* 'expected' and 'has' as in Kayvan's Core type checker *)
-  | NIA :
+  | Illtyped_binary_it of
+      { left : SurfaceBaseTypes.t Terms.term;
+        right : SurfaceBaseTypes.t Terms.term;
+        binop : CF.Cn.cn_binop
+      }
+  | NIA of
       { it : IT.t;
         hint : string
       }
-      -> message
   | TooBigExponent : { it : IT.t } -> message
   | NegativeExponent : { it : IT.t } -> message
   | Write_value_unrepresentable of
@@ -515,6 +518,24 @@ let pp_message te =
   | Empty_provenance ->
     let short = !^"Empty provenance" in
     { short; descr = None; state = None }
+  | Illtyped_binary_it { left; right; binop } ->
+    let short =
+      !^"Ill-typed application of binary operation"
+      ^^^ squotes (CF.Cn_ocaml.PpAil.pp_cn_binop binop)
+      ^^^ dot
+    in
+    let descr =
+      Some
+        (squotes (IT.pp left)
+         ^^^ !^"has type"
+         ^^^ squotes (SurfaceBaseTypes.pp (IT.bt left))
+         ^^ comma
+         ^^^ squotes (IT.pp right)
+         ^^^ !^"has type"
+         ^^^ squotes (SurfaceBaseTypes.pp (IT.bt right))
+         ^^ dot)
+    in
+    { short; descr; state = None }
 
 
 type t = type_error

backend/cn/wellTyped.ml

@@ -373,6 +373,9 @@ module WIT = struct
     | IT (Cons (it, _), _, _) | it -> return @@ IT.loc it
 
 
+  (* NOTE: This cannot _check_ what the root type of term is (the type is
+     universally quantified) and so is not suitable for catching incorrect
+     type annotations. *)
   let rec infer : 'bt. 'bt term -> BT.t term m =
     fun it ->
     Pp.debug 22 (lazy (Pp.item "Welltyped.WIT.infer" (IT.pp it)));

frontend/model/cn.lem

@@ -55,6 +55,7 @@ type cn_binop =
   | CN_and
   | CN_implies
   | CN_map_get
+  | CN_band
 
 
 (*

ocaml_frontend/cn_ocaml.ml

@@ -105,6 +105,7 @@ module MakePp (Conf: PP_CN) = struct
     | CN_and -> P.ampersand ^^ P.ampersand
     | CN_implies -> P.equals ^^ P.equals ^^ P.rangle
     | CN_map_get -> P.string "CN_map_get"
+    | CN_band -> P.ampersand
 
   let pp_cn_c_kind = function
     | C_kind_var -> !^ "c_var"

parsers/c/c_parser.mly

@@ -1938,9 +1938,11 @@ unary_expr:
 
 
 mul_expr:
-(* TODO *)
 | e= unary_expr
      { e }
+| e1= mul_expr AMPERSAND e2= unary_expr
+    { Cerb_frontend.Cn.(CNExpr ( Cerb_location.(region ($startpos, $endpos) (PointCursor $startpos($2)))
+                               , CNExpr_binop (CN_band, e1, e2))) }
 | e1= mul_expr STAR e2= unary_expr
     { Cerb_frontend.Cn.(CNExpr ( Cerb_location.(region ($startpos, $endpos) (PointCursor $startpos($2)))
                                , CNExpr_binop (CN_mul, e1, e2))) }

tests/cn/bitwise_and.c

@@ -1,5 +1,14 @@
+/*@
+function (bool) bw_and_precedence() {
+    let x = 0i32;
+    ~x & 0i32 == 0i32
+}
+@*/
+
 int main()
 {
+    /*@ assert (-1i32 & 0i32 == 0i32); @*/
+    /*@ assert (bw_and_precedence()); @*/
     int x = 0b110;
     int y = x & 0b101;
     /*@ assert(y == 4i32); @*/

tests/cn/bitwise_and_type_left.error.c

@@ -0,0 +1,5 @@
+int main()
+{
+    /*@ assert (0 & 1i32 == 0i32); @*/
+    return 0;
+}

tests/cn/bitwise_and_type_right.error.c

@@ -0,0 +1,5 @@
+int main()
+{
+    /*@ assert (0i32 & 1 == 0i32); @*/
+    return 0;
+}