Add support for shift-right on signed numbers.

Fixes #464

backend/cn/lib/check.ml

@@ -544,8 +544,9 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m =
              { loc; msg = Mismatch { has = BT.pp ty; expect = !^"comparable type" } })
        in
        let not_yet x =
-           Pp.debug 1 (lazy (Pp.item "not yet restored" (Pp_mucore_ast.pp_pexpr orig_pe)));
-           failwith ("todo: " ^ x) in
+         Pp.debug 1 (lazy (Pp.item "not yet restored" (Pp_mucore_ast.pp_pexpr orig_pe)));
+         failwith ("todo: " ^ x)
+       in
        (match op with
         | OpDiv ->
           let@ () = WellTyped.ensure_base_type loc ~expect (bt_of_pexpr pe1) in
@@ -625,8 +626,7 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m =
         | OpSub -> not_yet "OpSub"
         | OpMul -> not_yet "OpMul"
         | OpRem_f -> not_yet "OpRem_f"
-        | OpExp -> not_yet "OpExp"
-        )
+        | OpExp -> not_yet "OpExp")
      | M_PEapply_fun (fun_id, args) ->
        let@ () =
          match mu_fun_return_type fun_id args with
@@ -699,11 +699,10 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m =
        (* in integers, perform this op and round. in bitvector types, just perform
           the op (for all the ops where wrapping is consistent) *)
        let@ () = WellTyped.WCT.is_ct act.loc act.ct in
-       (*
        assert (
          match act.ct with
          | Integer ity when Sctypes.is_unsigned_integer_type ity -> true
-         | _ -> false); *)
+         | _ -> false);
        let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in
        let@ () = ensure_base_type loc ~expect (bt_of_pexpr pe1) in
        let@ () = WellTyped.ensure_bits_type loc expect in

backend/cn/lib/core_to_mucore.ml

@@ -341,23 +341,34 @@ let rec n_pexpr ~inherit_loc loc (Pexpr (annots, bty, pe)) : unit Mucore.mu_pexp
              ^^^ list CF.Pp_core.Basic.pp_pexpr args))
      | Sym sym, _ -> assert_error loc (!^"PEcall not inlined:" ^^^ Sym.pp sym)
      | Impl impl, args ->
-      (match impl, args with
-       | CF.Implementation.SHR_signed_negative, [Pexpr (_,_,PEval (Vctype ct)) ;arg1;arg2] ->
-         let arg1 = n_pexpr loc arg1 in
-         let arg2 = n_pexpr loc arg2 in
-         let ity = match Sctypes.is_integer_type (convert_ct loc ct) with
-                   | Some i -> i
-                   | None -> failwith "Non-integer type in shift" in
-         let act = ity_act loc ity in
-         let op = CF.Core.IOpShr in
-         let bound = M_Bound_Except act in
-         let shift = annotate (M_PEbounded_binop (bound,op,arg1,arg2)) in
-         annotate (M_PEerror ("Shifting a negative number to the right is implementation-dependant.",shift))
-       | _ -> assert_error
-         loc
-         (!^"PEcall to impl not inlined:"
-          ^^^ !^(CF.Implementation.string_of_implementation_constant impl))))
-
+       (match (impl, args) with
+        | ( CF.Implementation.SHR_signed_negative,
+            [ Pexpr (_, _, PEval (Vctype ct)); arg1; arg2 ] ) ->
+          let arg1 = n_pexpr loc arg1 in
+          let arg2 = n_pexpr loc arg2 in
+          let ity =
+            match Sctypes.is_integer_type (convert_ct loc ct) with
+            | Some i -> i
+            | None -> failwith "Non-integer type in shift"
+          in
+          let act = ity_act loc ity in
+          let op = CF.Core.IOpShr in
+          let bound = M_Bound_Except act in
+          let shift = annotate (M_PEbounded_binop (bound, op, arg1, arg2)) in
+          let impl_ok = true (* XXX: parameterize *) in
+          if impl_ok then
+            shift
+          else
+            annotate
+              (M_PEerror
+                 ( "Shifting a negative number to the right is implementation-dependant.",
+                   shift ))
+          (* XXX: Make a type for reporting implementation defined behavior? *)
+        | _ ->
+          assert_error
+            loc
+            (!^"PEcall to impl not inlined:"
+             ^^^ !^(CF.Implementation.string_of_implementation_constant impl))))
   | PElet (pat, e', e'') ->
     (match (pat, e') with
      | Pattern (_annots, CaseBase (Some sym, _)), Pexpr (annots2, _, PEsym sym2)

backend/cn/lib/mucore.mli

@@ -144,10 +144,12 @@ end
 
 type symbol = Cerb_frontend.Symbol.sym
 
+(** Annotated C type.  The annotations are typically an explanation of
+    something that might go wrong (e.g., overflow on an integer type). *)
 type act =
-  { loc : loc;
-    annot : Cerb_frontend.Annot.annot list;
-    ct : T.ct
+  { loc : loc; (** Source location *)
+    annot : Cerb_frontend.Annot.annot list; (** Annotations *)
+    ct : T.ct (** Affected type *)
   }
 
 type 'TY mu_object_value_ =
@@ -208,9 +210,11 @@ type bw_unop =
   | M_BW_CTZ
   | M_BW_FFS
 
+(** What to do on out of bounds.
+    The annotated C type is the result type of the operation. *)
 type bound_kind =
-  | M_Bound_Wrap of act
-  | M_Bound_Except of act
+  | M_Bound_Wrap of act (** Wrap around (used for unsigned types) *)
+  | M_Bound_Except of act (** Report an exception, for signed types *)
 
 val bound_kind_act : bound_kind -> act
 

frontend/model/translation.lem

@@ -1729,7 +1729,7 @@ else
                                Caux.mk_std_pe "6.5.7#5, sentence 3" begin
                                 Caux.mk_if_pe_ [Annot.Anot_explode] (Caux.mk_op_pe C.OpGe promoted1_wrp.E.sym_pe (Caux.mk_integer_pe 0))
   begin if Global.backend_name () = "Cn" then
-                                  Caux.mk_wrapI_pe result_ity C.IOpShr promoted1_wrp.E.sym_pe promoted2_wrp.E.sym_pe
+                                  Caux.mk_catch_exceptional_condition_pe result_ity C.IOpShr promoted1_wrp.E.sym_pe promoted2_wrp.E.sym_pe
   else
                                   expr
   end