GitLab will be upgraded on 30 Jan 2023 from 2.00 pm (AEDT) to 3.00 pm (AEDT). During the update, GitLab and Mattermost services will not be available. If you have any concerns with this, please talk to us at N110 (b) CSIT building.

basicMemoryOpsTestScript.sml 1.77 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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.
*)

16
val global_cell_test = uir_bundle`
17
18
19
20
21
22
23
24
25
26
  .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)
  } // .
27
28
` |> to_env |> start_at "main" `[IntV 8 4w]`
  |> run_schedule `single_thread_seq_cst_schedule`
29
  |> expect_result `OK (NOR [IntV 8 4w])`
30

31
val heap_alloc_test = uir_bundle`
32
33
34
35
36
37
38
39
40
41
  .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)
  } // .
42
43
` |> to_env |> start_at "main" `[IntV 8 4w]`
  |> run_schedule `single_thread_seq_cst_schedule`
44
  |> expect_result `OK (NOR [IntV 8 4w])`
45

46
val stack_alloc_test = uir_bundle`
47
48
49
50
51
52
53
54
55
56
  .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)
  } // .
57
58
` |> to_env |> start_at "main" `[IntV 8 4w]`
  |> run_schedule `single_thread_seq_cst_schedule`
59
  |> expect_result `OK (NOR [IntV 8 4w])`
60

61
62
val _ = export_theory()