CN: add bitwise and/or as no-smt ops

These are exactly analogous to XORNoSMT (in its various forms).

backend/cn/builtins.ml

@@ -36,6 +36,8 @@ let power_uf_def = ("power_uf", Sym.fresh_named "power_uf", mk_arg2 exp_no_smt_)
 let rem_uf_def = ("rem_uf", Sym.fresh_named "rem_uf", mk_arg2 rem_no_smt_)
 let mod_uf_def = ("mod_uf", Sym.fresh_named "mod_uf", mk_arg2 mod_no_smt_)
 let xor_uf_def = ("xor_uf", Sym.fresh_named "xor_uf", mk_arg2 xor_no_smt_)
+let bw_and_uf_def = ("bw_and_uf", Sym.fresh_named "bw_and_uf", mk_arg2 bw_and_no_smt_)
+let bw_or_uf_def = ("bw_or_uf", Sym.fresh_named "bw_or_uf", mk_arg2 bw_or_no_smt_)
 
 let power_def = ("power", Sym.fresh_named "power", mk_arg2 exp_)
 let rem_def = ("rem", Sym.fresh_named "rem", mk_arg2 rem_)
@@ -77,6 +79,8 @@ let builtin_funs =
       rem_uf_def;  
       mod_uf_def;
       xor_uf_def;
+      bw_and_uf_def;
+      bw_or_uf_def;
 
       power_def;
       rem_def;

backend/cn/check.ml

@@ -543,10 +543,26 @@ let rec check_pexpr (pe : 'bty mu_pexpr) ~(expect:BT.t)
      end
   | M_CivCOMPL _ ->
      Cerb_debug.error "todo: CivCOMPL"
-  | M_CivAND _ ->
-     Cerb_debug.error "todo: CivAND"
-  | M_CivOR _ ->
-     Cerb_debug.error "todo: CivOR"
+  | M_CivAND (act, pe1, pe2) ->
+     let@ () = WellTyped.ensure_base_type loc ~expect Integer in
+     let _ity = match act.ct with
+       | Integer ity -> ity
+       | _ -> Cerb_debug.error "M_CivAND with non-integer c-type"
+     in
+     check_pexpr ~expect:Integer pe1 (fun vt1 ->
+     check_pexpr ~expect:Integer pe2 (fun vt2 ->
+     let value = warn_uf loc "bw_and_uf"; bw_and_no_smt_ (vt1, vt2) in
+     k value))
+  | M_CivOR (act, pe1, pe2) ->
+     let@ () = WellTyped.ensure_base_type loc ~expect Integer in
+     let _ity = match act.ct with
+       | Integer ity -> ity
+       | _ -> Cerb_debug.error "M_CivOR with non-integer c-type"
+     in
+     check_pexpr ~expect:Integer pe1 (fun vt1 ->
+     check_pexpr ~expect:Integer pe2 (fun vt2 ->
+     let value = warn_uf loc "bw_or_uf"; bw_or_no_smt_ (vt1, vt2) in
+     k value))
   | M_CivXOR (act, pe1, pe2) -> 
      let@ () = WellTyped.ensure_base_type loc ~expect Integer in
      let _ity = match act.ct with

backend/cn/indexTerms.ml

@@ -435,6 +435,8 @@ let max_ (it, it') = IT (Binop (Max,it, it'), bt it)
 let intToReal_ it = IT (Cast (Real, it), BT.Real)
 let realToInt_ it = IT (Cast (Integer, it), BT.Integer)
 let xor_no_smt_ (it, it') = IT (Binop (XORNoSMT,it, it'), bt it)
+let bw_and_no_smt_ (it, it') = IT (Binop (BWAndNoSMT,it, it'), bt it)
+let bw_or_no_smt_ (it, it') = IT (Binop (BWOrNoSMT,it, it'), bt it)
 
 let (%+) t t' = add_ (t, t')
 let (%-) t t' = sub_ (t, t')

backend/cn/solver.ml

@@ -53,6 +53,8 @@ let exp_no_smt_solver_sym = Sym.fresh_named "power_uf"
 let mod_no_smt_solver_sym = Sym.fresh_named "mod_uf"
 let rem_no_smt_solver_sym = Sym.fresh_named "rem_uf"
 let xor_no_smt_solver_sym = Sym.fresh_named "xor_uf"
+let bw_and_no_smt_solver_sym = Sym.fresh_named "bw_and_uf"
+let bw_or_no_smt_solver_sym = Sym.fresh_named "bw_or_uf"
 
 
 
@@ -483,6 +485,10 @@ module Translate = struct
          | Max -> term (ite_ (ge_ (t1, t2), t1, t2))
          | XORNoSMT ->
             make_uf xor_no_smt_solver_sym (Integer) [t1; t2]
+         | BWAndNoSMT ->
+            make_uf bw_and_no_smt_solver_sym (Integer) [t1; t2]
+         | BWOrNoSMT ->
+            make_uf bw_or_no_smt_solver_sym (Integer) [t1; t2]
          | EQ -> Z3.Boolean.mk_eq context
             (maybe_record_loc_addr_eq global t1 (term t1))
             (maybe_record_loc_addr_eq global t2 (term t2))

backend/cn/terms.ml

@@ -31,6 +31,8 @@ type binop =
   | Mod
   | ModNoSMT
   | XORNoSMT
+  | BWAndNoSMT
+  | BWOrNoSMT
   | LT
   | LE
   | Min
@@ -173,6 +175,10 @@ let pp : 'bt 'a. ?atomic:bool -> ?f:('bt term -> Pp.doc -> Pp.doc) -> 'bt term -
           c_app !^"max" [aux false it1; aux false it2]
        | XORNoSMT ->
           c_app !^"xor_uf" [aux false it1; aux false it2]
+       | BWAndNoSMT ->
+          c_app !^"bw_and_uf" [aux false it1; aux false it2]
+       | BWOrNoSMT ->
+          c_app !^"bw_or_uf" [aux false it1; aux false it2]
        | SetMember ->
           c_app !^"member" [aux false it1; aux false it2]
        | SetUnion ->

backend/cn/wellTyped.ml

@@ -234,10 +234,15 @@ module WIT = struct
                let hint = "Only exponentiation of two constants is allowed" in
                fail (fun ctxt -> {loc; msg = NIA {it = exp_ (t, t'); ctxt; hint}})
             end
-           | ExpNoSMT ->
+           | ExpNoSMT
+           | RemNoSMT
+           | ModNoSMT
+           | XORNoSMT
+           | BWAndNoSMT
+           | BWOrNoSMT ->
               let@ t = check loc Integer t in
               let@ t' = check loc Integer t' in
-              return (exp_no_smt_ (t, t'))
+              return (IT (Binop (arith_op, t, t'), Integer))
            | Rem ->
               let@ simp_ctxt = simp_ctxt () in
               let@ t = check loc Integer t in
@@ -249,10 +254,6 @@ module WIT = struct
               | Some z' ->
                  return (IT (Binop (Rem, t, z_ z'), Integer))
               end
-           | RemNoSMT ->
-              let@ t = check loc Integer t in
-              let@ t' = check loc Integer t' in
-              return (IT (Binop (RemNoSMT, t, t'), Integer))
            | Mod ->
               let@ simp_ctxt = simp_ctxt () in
               let@ t = check loc Integer t in
@@ -264,10 +265,6 @@ module WIT = struct
               | Some z' ->
                  return (IT (Binop (Mod, t, z_ z'), Integer))
               end
-           | ModNoSMT ->
-              let@ t = check loc Integer t in
-              let@ t' = check loc Integer t' in
-              return (IT (Binop (ModNoSMT, t, t'), Integer))
            | LT ->
               let@ t = infer loc t in
               let@ () = ensure_integer_or_real_type loc t in
@@ -288,10 +285,6 @@ module WIT = struct
               let@ () = ensure_integer_or_real_type loc t in
               let@ t' = check loc (IT.bt t) t' in
               return (IT (Binop (Max, t, t'), IT.bt t))
-           | XORNoSMT ->
-              let@ t = check loc Integer t in
-              let@ t' = check loc Integer t' in
-              return (IT (Binop (XORNoSMT, t, t'), BT.Integer))
            | EQ ->
               let@ t = infer loc t in
               let@ t' = check loc (IT.bt t) t' in