Bounded integer transformation

bin/asl2c.py

@@ -145,6 +145,13 @@
 // introduced by previous transforms
 :xform_constprop --nounroll
 
+// Optimization: optionally use :xform_bounded to represent any
+// constrained integers by an integer that is exactly the right size
+// to contain it.
+// This should come at the end of all the transformations because it changes
+// the types of functions.
+{bounded_int}
+
 // To let the generated code call your own functions, you need to declare
 // the type of an ASL function with a matching type and provide a configuration
 // file containing a list of these external functions.
@@ -313,6 +320,7 @@ def mk_script(args, output_directory):
         script = []
         script.append(":filter_unlisted_functions imports")
         script.append(":filter_reachable_from exports")
+        if args.Obounded: script.append(":xform_bounded")
         if args.show_final_asl:
             script.append(f":show --format=raw")
         else:
@@ -343,6 +351,10 @@ def mk_script(args, output_directory):
         substitutions['auto_case_split'] = '--no-auto-case-split'
     else:
         substitutions['auto_case_split'] = '--auto-case-split'
+    if args.Obounded:
+        substitutions['bounded_int'] = ':xform_bounded'
+    else:
+        substitutions['bounded_int'] = ''
     if not args.line_info:
         substitutions['line_info'] = '--no-line-info'
     else:
@@ -397,15 +409,16 @@ def generate_config_file(config_file, exports, imports):
         print("}", file=f)
     report(f"# Generated configuration file {config_file}\n")
 
-def run_asli(asli, runtime_checks, asl_files, project_file, configurations):
+def run_asli(asli, args, asl_files, project_file, configurations):
     asli_cmd = [
         asli,
         "--batchmode", "--nobanner",
     ]
     asli_cmd.append("--check-call-markers")
     asli_cmd.append("--check-exception-markers")
     asli_cmd.append("--check-constraints")
-    asli_cmd.append("--runtime-checks" if runtime_checks else "--no-runtime-checks")
+    asli_cmd.append("--runtime-checks" if args.runtime_checks else "--no-runtime-checks")
+    if args.Obounded: asli_cmd.append("--exec=:xform_bounded")
     asli_cmd.append(f"--project={project_file}")
     for file in configurations:
         asli_cmd.append(f"--configuration={file}")
@@ -501,6 +514,7 @@ def main() -> int:
     parser.add_argument("--instrument-unknown", help="instrument assignments of UNKNOWN", action=argparse.BooleanOptionalAction)
     parser.add_argument("--wrap-variables", help="wrap global variables into functions", action=argparse.BooleanOptionalAction)
     parser.add_argument("-O0", help="perform minimal set of transformations", action=argparse.BooleanOptionalAction)
+    parser.add_argument("-Obounded", help="enable integer bounding optimization", action="store_true", default=False)
     parser.add_argument("--backend", help="select backend (default: orig)", choices=['ac', 'c23', 'interpreter', 'fallback', 'orig', 'sc'], default='orig')
     parser.add_argument("--print-c-flags", help="print the C flags needed to use the selected ASL C runtime", action=argparse.BooleanOptionalAction)
     parser.add_argument("--print-ld-flags", help="print the Linker flags needed to use the selected ASL C runtime", action=argparse.BooleanOptionalAction)
@@ -556,6 +570,7 @@ def main() -> int:
         asli_cmd.append("--check-exception-markers")
         asli_cmd.append("--check-constraints")
         asli_cmd.append("--runtime-checks" if args.runtime_checks else "--no-runtime-checks")
+        if args.Obounded: asli_cmd.append("--exec=:xform_bounded")
         asli_cmd.extend([
             "--exec=let result = main();",
             "--exec=:quit",
@@ -570,7 +585,7 @@ def main() -> int:
         (project_file, config_filename, c_files, exe_file) = mk_filenames(backend, working_directory, args.basename, args.generate_cxx)
         generate_project(project_file, script)
         generate_config_file(config_filename, ["main"] + args.exports, args.imports)
-        run_asli(asli, args.runtime_checks, args.asl_files, project_file, [config_filename]+args.configuration)
+        run_asli(asli, args, args.asl_files, project_file, [config_filename]+args.configuration)
         if args.show_final_asl:
             pass
         elif args.run:

libASL/backend_c_new.ml

@@ -1310,6 +1310,40 @@ let mk_ffi_conversion (loc : Loc.t) (indirect : bool) (c_name : Ident.t) (asl_na
   let module Runtime = (val (!runtime) : RuntimeLib) in
   let pp_asl_name (fmt : PP.formatter) : unit = ident fmt asl_name in
   let pp_c_name (fmt : PP.formatter) : unit = ptr fmt (); ident fmt c_name in
+  let mk_ffi_convert_small_bits (n : int) =
+    { asl_name = asl_name;
+      asl_type = asl_type;
+      c_name = c_name;
+      pp_c_type = Some (fun fmt -> PP.fprintf fmt "uint%d_t" n);
+      pp_c_decl = (fun fmt ->
+        PP.fprintf fmt "uint%d_t %a%a" n ptr () ident c_name);
+      pp_asl_to_c = (fun fmt ->
+        PP.fprintf fmt "%a%a = %a;"
+          ptr ()
+          ident c_name
+          (Runtime.ffi_asl2c_bits_small n) pp_asl_name);
+      pp_c_to_asl = (fun fmt ->
+        varty loc fmt asl_name asl_type;
+        PP.fprintf fmt " = %a;"
+          (Runtime.ffi_c2asl_bits_small n) pp_c_name);
+    }
+  in
+  let mk_ffi_convert_large_bits (n : int) =
+    let chunks = (n+63) / 64 in
+    { asl_name = asl_name;
+      asl_type = asl_type;
+      c_name = c_name;
+      pp_c_type = None;
+      pp_c_decl = (fun fmt ->
+        PP.fprintf fmt "uint64_t %a[%d]"
+          ident c_name
+          chunks);
+      pp_asl_to_c = (fun fmt ->
+        Runtime.ffi_asl2c_bits_large fmt n pp_c_name pp_asl_name);
+      pp_c_to_asl = (fun fmt ->
+        Runtime.ffi_c2asl_bits_large fmt n pp_asl_name pp_c_name);
+    }
+  in
   ( match asl_type with
   | Type_Constructor (tc, []) when Ident.equal tc boolean_ident ->
       (* No conversion needed for boolean type since we use stdbool.h's bool already *)
@@ -1380,40 +1414,17 @@ let mk_ffi_conversion (loc : Loc.t) (indirect : bool) (c_name : Ident.t) (asl_na
           PP.fprintf fmt " = %a;"
             Runtime.ffi_c2asl_sintN_small pp_c_name);
       }
-  | Type_Bits(Expr_Lit (VInt n), _) when List.mem (Z.to_int n) [8; 16; 32; 64] ->
-      let n' = Z.to_int n in
-      { asl_name = asl_name;
-        asl_type = asl_type;
-        c_name = c_name;
-        pp_c_type = Some (fun fmt -> PP.fprintf fmt "uint%d_t" n');
-        pp_c_decl = (fun fmt ->
-          PP.fprintf fmt "uint%d_t %a%a" n' ptr () ident c_name);
-        pp_asl_to_c = (fun fmt ->
-          PP.fprintf fmt "%a%a = %a;"
-            ptr ()
-            ident c_name
-            (Runtime.ffi_asl2c_bits_small n') pp_asl_name);
-        pp_c_to_asl = (fun fmt ->
-          varty loc fmt asl_name asl_type;
-          PP.fprintf fmt " = %a;"
-            (Runtime.ffi_c2asl_bits_small n') pp_c_name);
-      }
-  | Type_Bits(Expr_Lit (VInt n), _) ->
-      let n' = Z.to_int n in
-      let chunks = (n'+63) / 64 in
-      { asl_name = asl_name;
-        asl_type = asl_type;
-        c_name = c_name;
-        pp_c_type = None;
-        pp_c_decl = (fun fmt ->
-          PP.fprintf fmt "uint64_t %a[%d]"
-            ident c_name
-            chunks);
-        pp_asl_to_c = (fun fmt ->
-          Runtime.ffi_asl2c_bits_large fmt (Z.to_int n) pp_c_name pp_asl_name);
-        pp_c_to_asl = (fun fmt ->
-          Runtime.ffi_c2asl_bits_large fmt (Z.to_int n) pp_asl_name pp_c_name);
-      }
+  | Type_Bits(Expr_Lit (VInt n), _)
+    when List.mem (Z.to_int n) [8; 16; 32; 64]
+    -> mk_ffi_convert_small_bits (Z.to_int n)
+  | Type_Bits(Expr_TApply (f, _, [Expr_Lit (VIntN n)], _), _)
+    when Ident.equal f cvt_sintN_int && List.mem (Z.to_int n.v) [8; 16; 32; 64]
+    -> mk_ffi_convert_small_bits (Z.to_int n.v)
+  | Type_Bits(Expr_Lit (VInt n), _)
+    -> mk_ffi_convert_large_bits (Z.to_int n)
+  | Type_Bits(Expr_TApply (f, _, [Expr_Lit (VIntN n)], _), _)
+    when Ident.equal f cvt_sintN_int
+    -> mk_ffi_convert_large_bits (Z.to_int n.v)
   | _ ->
       let msg = PP.asprintf "Type '%a' cannot be used in functions that are imported or exported between ASL and C"
         FMT.ty asl_type

libASL/dune

@@ -62,6 +62,7 @@
    check_monomorphization
    xform_bitslices
    xform_bittuples
+   xform_bounded
    xform_case
    xform_constprop
    xform_desugar