Verify SRTL gas consumption for transition executions

tests/runner/Testcontracts.ml

@@ -60,13 +60,93 @@ let output_test_result env test_ctxt test_name ipc_mode goldoutput_file msg out
     let gold_output = normalize_json non_normalized_gold_output in
     output_verifier gold_output msg (env.print_diff test_ctxt) out
 
-let foutput env test_ctxt test_name ipc_mode ipc_addr_thread exit_code
-    output_file goldoutput_file msg s =
+let gas_rem_from_output outs'' =
+  let outs' = String.split_on_chars ~on:[ '\n' ] outs'' in
+  match
+    List.find_map outs' ~f:(fun outs ->
+        let re =
+          Str.regexp ".*\"gas_remaining\"[\\t ]*:[\\t ]*\"\\([0-9]+\\)\".*"
+        in
+        match Str.string_match re outs 0 with
+        | true -> Some (Str.matched_group 1 outs)
+        | false -> (
+            let re = Str.regexp ".*Gas remaining:[\\t ]*\\([0-9]+\\).*" in
+            match Str.string_match re outs 0 with
+            | true -> Some (Str.matched_group 1 outs)
+            | false -> None))
+  with
+  | Some nums -> Int.of_string nums
+  | None -> 0
+
+let test_compiled_scilla_gas env test_ctxt name test_id init_name exit_code
+    expected_remaining_gas =
+  let istr = Int.to_string test_id in
+  let tests_dir =
+    FilePath.make_relative (Sys.getcwd ()) (env.tests_dir test_ctxt)
+  in
+  let contract_dir = tests_dir ^/ "contracts" in
+  let dir = tests_dir ^/ "runner" ^/ name in
+  let tmpdir = bracket_tmpdir test_ctxt in
+  let ll_file = tmpdir ^/ name ^ istr ^. "ll" in
+  let init_file = dir ^/ init_name ^. "json" in
+  let compiler_args =
+    [
+      "-init";
+      init_file;
+      contract_dir ^/ name ^. "scilla";
+      (* stdlib is in src/stdlib *)
+      "-libdir";
+      env.stdlib_dir test_ctxt;
+      "-o";
+      ll_file;
+      "-gaslimit";
+      testsuit_gas_limit;
+    ]
+  in
+  let rtl_runner_args =
+    [
+      "-i";
+      ll_file;
+      "-n";
+      init_file;
+      "-g";
+      testsuit_gas_limit;
+      "-b";
+      dir ^/ "blockchain_" ^ istr ^. "json";
+      "-m";
+      dir ^/ "message_" ^ istr ^. "json";
+      "-s";
+      dir ^/ "state_" ^ istr ^. "json";
+    ]
+  in
+  let compiler_bin_o = env.scilla_compiler_bin test_ctxt in
+  match compiler_bin_o with
+  | Some compiler_bin ->
+      assert_command ~exit_code:succ_code ~use_stderr:true ~ctxt:test_ctxt
+        compiler_bin compiler_args;
+      let srtl_runner_bin_o = env.scilla_rtl_runner_bin test_ctxt in
+      assert_bool "Compiler bin provided but not SRTL runner"
+        (Option.is_some srtl_runner_bin_o);
+      (* We now have the LLVM IR for this, execute it. *)
+      assert_command ~exit_code ~use_stderr:true ~ctxt:test_ctxt
+        (Option.value_exn srtl_runner_bin_o) rtl_runner_args
+        ~foutput:(fun runnerout ->
+          let srtl_gasrem = gas_rem_from_output (stream_to_string runnerout) in
+          assert_bool
+            (sprintf "Expected gas remaining vs SRTL gas remaining: %d %d"
+               expected_remaining_gas srtl_gasrem)
+            (srtl_gasrem = expected_remaining_gas))
+  | None -> ()
+
+let foutput compiled_scilla_tester env test_ctxt test_name ipc_mode
+    ipc_addr_thread exit_code output_file goldoutput_file msg s =
   (* if the test is supposed to succeed we read the output from a file,
      otherwise we read from the output stream *)
   let interpreter_output =
     get_interpreter_output env test_ctxt exit_code output_file s
   in
+  let interpreter_gas_rem = gas_rem_from_output interpreter_output in
+  compiled_scilla_tester exit_code interpreter_gas_rem;
   let out =
     if ipc_mode then
       (* The output of the interpreter in IPC mode will only contain "_balance" as
@@ -174,10 +254,13 @@ let rec build_contract_tests_with_init_file ?(pplit = true) env name exit_code i
           [ "run"; "-argv"; String.concat args ~sep:" " ]
         else args
       in
+      let compiled_scilla_tester =
+        test_compiled_scilla_gas env test_ctxt name i init_name
+      in
       assert_command ~exit_code ~use_stderr:true ~ctxt:test_ctxt runner args
         ~foutput:
-          (foutput env test_ctxt test_name ipc_mode ipc_addr_thread exit_code
-             output_file goldoutput_file msg)
+          (foutput compiled_scilla_tester env test_ctxt test_name ipc_mode
+             ipc_addr_thread exit_code output_file goldoutput_file msg)
     in
     (* If this test is expected to succeed, we know that the JSONs are all "good".
      * So test both the JSON parsers, one that does validation, one that doesn't.

tests/util/Util.ml

@@ -41,6 +41,8 @@ type tsuite_env = {
   print_diff : test_ctxt -> bool;
   ext_ipc_server : test_ctxt -> string;
   server : test_ctxt -> bool;
+  scilla_compiler_bin : test_ctxt -> string option;
+  scilla_rtl_runner_bin : test_ctxt -> string option;
 }
 
 let run_tests tests =
@@ -72,7 +74,16 @@ let run_tests tests =
       "Address of external IPC server for IPC tests. Ensure that \"-runner \
        sequential\" is set"
   in
-
+  let scilla_compiler_bin =
+    Conf.make_string_opt "scilla_compiler_bin" None
+      "Path to scilla compiler bin if compiled Scilla must be checked for gas \
+       compatbility"
+  in
+  let scilla_rtl_runner_bin =
+    Conf.make_string_opt "scilla_rtl_runner_bin" None
+      "Path to scilla runner bin (SRTL) if compiled Scilla must be checked for \
+       gas compatbility"
+  in
   let env : tsuite_env =
     {
       tests_dir;
@@ -82,6 +93,8 @@ let run_tests tests =
       print_diff;
       server;
       ext_ipc_server;
+      scilla_compiler_bin;
+      scilla_rtl_runner_bin;
     }
   in
   run_test_tt_main ("tests" >::: List.map ~f:(( |> ) env) tests)