[asl] Use more constraints in stdlib.asl

asllib/Native.ml

@@ -316,8 +316,18 @@ module NativeBackend = struct
     let round_towards_zero = wrap_real_to_int "RoundTowardsZero" truncate
 
     let primitives =
+      let e_var x = E_Var x |> add_dummy_pos in
+      let eoi i = expr_of_int i in
+      let binop = ASTUtils.binop in
+      let minus_one e = binop MINUS e (eoi 1) in
+      let pow_2 = binop POW (eoi 2) in
+      let neg e = E_Unop (NEG, e) |> add_pos_from e in
       (* [t_bits "N"] is the bitvector type of length [N]. *)
-      let t_bits x = T_Bits (E_Var x |> add_dummy_pos, []) |> add_dummy_pos in
+      let t_bits x = T_Bits (e_var x, []) |> add_dummy_pos in
+      (* [t_int_ctnt e1 e2] is [integer {e1..e2}] *)
+      let t_int_ctnt e1 e2 =
+        T_Int (WellConstrained [ Constraint_Range (e1, e2) ]) |> add_dummy_pos
+      in
       (* [p ~parameters ~args ~returns name f] declares a primtive named [name]
          with body [f], and signature specified by [parameters] [args] and
          [returns]. *)
@@ -329,14 +339,22 @@ module NativeBackend = struct
         ({ name; parameters; args; body; return_type; subprogram_type }, f)
       in
       [
-        p
-          ~parameters:[ ("N", None) ]
-          ~args:[ ("x", t_bits "N") ]
-          ~returns:integer "UInt" uint;
-        p
-          ~parameters:[ ("N", None) ]
-          ~args:[ ("x", t_bits "N") ]
-          ~returns:integer "SInt" sint;
+        (let two_pow_n_minus_one = minus_one (pow_2 (e_var "N")) in
+         let returns = t_int_ctnt (eoi 0) two_pow_n_minus_one in
+         p
+           ~parameters:[ ("N", None) ]
+           ~args:[ ("x", t_bits "N") ]
+           ~returns "UInt" uint);
+        (let two_pow_n_minus_one = pow_2 (minus_one (e_var "N")) in
+         let minus_two_pow_n_minus_one = neg two_pow_n_minus_one
+         and two_pow_n_minus_one_minus_one = minus_one two_pow_n_minus_one in
+         let returns =
+           t_int_ctnt minus_two_pow_n_minus_one two_pow_n_minus_one_minus_one
+         in
+         p
+           ~parameters:[ ("N", None) ]
+           ~args:[ ("x", t_bits "N") ]
+           ~returns "SInt" sint);
         p ~args:[ ("x", integer) ] ~returns:string "DecStr" dec_str;
         p ~args:[ ("x", integer) ] ~returns:string "HexStr" hex_str;
         p ~args:[ ("x", integer) ] ~returns:string "AsciiStr" ascii_str;

herd/ASLSem.ml

@@ -648,6 +648,9 @@ module Make (C : Config) = struct
       let open AST in
       let with_pos = Asllib.ASTUtils.add_dummy_pos in
       let integer = Asllib.ASTUtils.integer in
+      let int_ctnt e1 e2 =
+        T_Int (WellConstrained [ Constraint_Range (e1, e2) ]) |> with_pos
+      in
       let boolean = Asllib.ASTUtils.boolean in
       let reg = integer in
       let var x = E_Var x |> with_pos in
@@ -656,7 +659,16 @@ module Make (C : Config) = struct
       let bv_var x = bv @@ var x in
       let bv_lit x = bv @@ lit x in
       let bv_64 = bv_lit 64 in
+      let binop = Asllib.ASTUtils.binop in
+      let minus_one e = binop MINUS e (lit 1) in
+      let pow_2 = binop POW (lit 2) in
       let t_named x = T_Named x |> with_pos in
+      let uint_returns =
+        int_ctnt (lit 0) (minus_one (pow_2 (var "N")))
+      and sint_returns =
+        let big_pow = pow_2 (minus_one (var "N")) in
+        int_ctnt (E_Unop(NEG, big_pow) |> with_pos) (minus_one big_pow)
+      in
       [
 (* Fences *)
         p0 "primitive_isb" (primitive_isb ii_env);
@@ -686,11 +698,11 @@ module Make (C : Config) = struct
          p1r "UInt"
           ~parameters:[ ("N", None) ]
           ("x", bv_var "N")
-          ~returns:integer uint;
+          ~returns:uint_returns uint;
         p1r "SInt"
           ~parameters:[ ("N", None) ]
           ("x", bv_var "N")
-          ~returns:integer sint;
+          ~returns:sint_returns sint;
 (* Misc *)
         p0r "ProcessorID" ~returns:integer (processor_id ii_env);
         p2r "CanPredictFrom"