open HolKernel Parse boolLib bossLib

open uvmSchedulerTheory
open wordsLib
open BundleParser
open EvalUtils

val _ = new_theory "basicMemoryOpsTest"
val _ = add_extra_eval_thms()

(* `// .` and `// .).)` are comments used to fix Vim syntax highlighting. The
   syntax file doesn't understand that the quoted UIR code is not HOL code, and
   attempts to parse @ as ∀. These comments can be safely ignored.
*)

val global_cell_test = uir_bundle`
  .typedef @i8 = int<8>
  .global @g <@i8>
  .funcsig @main_sig = (@i8) -> (@i8) // .).)
  .funcdef @main VERSION %v1 <@main_sig> { // .
    %entry(<@i8> %a):
      %ig = GETIREF <@i8> @g // .
      STORE SEQ_CST <@i8> %ig %a
      %b = LOAD SEQ_CST <@i8> %ig
      RET (%b)
  } // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
  |> run_schedule `single_thread_seq_cst_schedule`
  |> expect_result `OK (NOR [IntV 8 4w])`

val heap_alloc_test = uir_bundle`
  .typedef @i8 = int<8>
  .funcsig @main_sig = (@i8) -> (@i8) // .).)
  .funcdef @main VERSION %v1 <@main_sig> { // .
    %entry(<@i8> %a):
      %heap = NEW <@i8>
      %i = GETIREF <@i8> %heap
      STORE SEQ_CST <@i8> %i %a
      %b = LOAD SEQ_CST <@i8> %i
      RET (%b)
  } // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
  |> run_schedule `single_thread_seq_cst_schedule`
  |> expect_result `OK (NOR [IntV 8 4w])`

val stack_alloc_test = uir_bundle`
  .typedef @i8 = int<8>
  .funcsig @main_sig = (@i8) -> (@i8) // .).)
  .funcdef @main VERSION %v1 <@main_sig> { // .
    %entry(<@i8> %a):
      %stack = ALLOCA <@i8>
      %i = GETIREF <@i8> %stack
      STORE SEQ_CST <@i8> %i %a
      %b = LOAD SEQ_CST <@i8> %i
      RET (%b)
  } // .
` |> to_env |> start_at "main" `[IntV 8 4w]`
  |> run_schedule `single_thread_seq_cst_schedule`
  |> expect_result `OK (NOR [IntV 8 4w])`

val _ = export_theory()