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.

codeTestScript.sml 4.84 KB
Newer Older
Adam R. Nelson's avatar
Adam R. Nelson committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
open HolKernel Parse boolLib bossLib

open ParserHelpers
open TypeParser
open ValueParser
open CodeParser
open wordsTheory
open sumMonadTheory
open uvmTypesTheory
open uvmValuesTheory
open uvmMemoryTheory
open uvmIRTheory

val _ = new_theory "codeTest"

fun assert_parse_inst(s, i) =
  let val i' = uir_inst mock_context [QUOTE ("(* *)" ^ s)]
        handle HOL_ERR e => raise ParseError(
          "failed to parse inst '" ^ s ^ "': " ^ #message e)
  in
    prove(mk_eq(i', mk_return i),
      simp[lift_left_def, ap_left_def, mapM_left_def, sequence_left_def])
    handle HOL_ERR e => raise ParseError(
      "inst '" ^ s ^ "' did not parse as (" ^ term_to_string i ^ "): " ^ #message e)
  end

fun assert_parse_terminst(s, i) =
  let val i' = uir_terminst mock_context [QUOTE ("(* *)" ^ s)]
        handle HOL_ERR e => raise ParseError(
          "failed to parse terminst '" ^ s ^ "': " ^ #message e)
  in
    prove(mk_eq(i', mk_return i),
      rw[get_callee_def] >> simp[lift_left_def, ap_left_def, mapM_left_def, sequence_left_def])
    handle HOL_ERR e => (
      print (type_to_string (type_of i') ^ "; " ^ type_to_string (type_of i));
      raise ParseError(
        "terminst '" ^ s ^ "' did not parse as (" ^ term_to_string i ^ "): " ^ #message e))
  end

val _ =
  assert_parse_inst("ID <int<8>> %bar",
42
    ``Assign [] (Id (Int 8) (Var %"bar"))``);
Adam R. Nelson's avatar
Adam R. Nelson committed
43
  assert_parse_inst("%foo = ID <int<8>> %bar",
44
    ``Assign [%"foo"] (Id (Int 8) (Var %"bar"))``);
Adam R. Nelson's avatar
Adam R. Nelson committed
45
  assert_parse_inst("(%foo %bar) = ID <int<8>> %baz",
46
    ``Assign [%"foo"; %"bar"] (Id (Int 8) (Var %"baz"))``);
Adam R. Nelson's avatar
Adam R. Nelson committed
47
  assert_parse_inst("ADD <int<8>> %a %b",
48
    ``Assign [] (BinOp ADD (Int 8) (Var %"a") (Var %"b"))``);
Adam R. Nelson's avatar
Adam R. Nelson committed
49
  assert_parse_inst("UGT <int<8>> %a %b",
50
    ``Assign [] (CmpOp UGT (Int 8) (Var %"a") (Var %"b"))``);
Adam R. Nelson's avatar
Adam R. Nelson committed
51
  assert_parse_inst("TRUNC <int<8> int<16>> %a",
52
    ``Assign [] (ConvOp TRUNC (Int 8) (Int 16) (Var %"a"))``);
Adam Nelson's avatar
Adam Nelson committed
53
  assert_parse_inst("%th = NEWTHREAD %st THROW_EXC %ex",
54
55
    ``NewThread (%"th") (Var %"st") (Const (RefV Void NONE))
        (ThrowExc (Var %"ex"))``);
Adam Nelson's avatar
Adam Nelson committed
56
  assert_parse_inst("%th = NEWTHREAD %st PASS_VALUES <int<8> int<16>> (%a %b)",
57
58
59
60
    ``NewThread (%"th") (Var %"st") (Const (RefV Void NONE))
        (PassValues [(Var %"a", Int 8); (Var %"b", Int 16)])``);
  assert_parse_terminst("RET (%foo %bar)", ``Ret [Var %"foo"; Var %"bar"]``);
  assert_parse_terminst("THROW %foo", ``Throw (Var %"foo")``);
Adam R. Nelson's avatar
Adam R. Nelson committed
61
  assert_parse_terminst("BRANCH %label(%a %b)",
62
    ``Branch1 (BlockLabel "label", [Var %"a"; Var %"b"])``);
Adam R. Nelson's avatar
Adam R. Nelson committed
63
  assert_parse_terminst("BRANCH2 %cond %t() %f()",
64
    ``Branch2 (Var %"cond") (BlockLabel "t", []) (BlockLabel "f", [])``);
Adam R. Nelson's avatar
Adam R. Nelson committed
65
66
  assert_parse_terminst("TAILCALL <(int<8>) -> ()> %fn (%arg)",
    ``TailCall <|
67
68
69
        name := INL %"fn";
        args := [Var %"arg"];
        signature := <|arg_types := [Int 8]; return_types := []|>;
Adam R. Nelson's avatar
Adam R. Nelson committed
70
71
72
        convention := Mu
      |>``);
  assert_parse_terminst("CALL <(int<8>) -> ()> %fn (%arg) EXC (%n() %e())",
73
74
75
76
    ``Call [] <|
        name := INL %"fn";
        args := [Var %"arg"];
        signature := <|arg_types := [Int 8]; return_types := []|>;
Adam R. Nelson's avatar
Adam R. Nelson committed
77
78
79
        convention := Mu
      |> <|
        normal_dest := (BlockLabel "n", []);
80
        exceptional_dest := SOME (BlockLabel "e", [])
Adam R. Nelson's avatar
Adam R. Nelson committed
81
      |>``);
82
83
84
85
86
87
88
89
90
91
  assert_parse_terminst("%x = CALL <(int<8>) -> (int<8>)> %fn (%arg) EXC (%n(%x) %e())",
    ``Call [%"x"] <|
        name := INL %"fn";
        args := [Var %"arg"];
        signature := <|arg_types := [Int 8]; return_types := [Int 8]|>;
        convention := Mu
      |> <|
        normal_dest := (BlockLabel "n", [Var %"x"]);
        exceptional_dest := SOME (BlockLabel "e", [])
      |>``);
92
93
94
95
96
97
98
99
100
101
102
  assert_parse_terminst("%x = COMMINST @uvm.new_stack <[@sig]> (%st) EXC (%n(%x))",
    ``CommInst [%"x"] (NewStack <|arg_types := []; return_types := []|> (Var %"st"))
      <| normal_dest := (BlockLabel "n", [Var %"x"]);
         exceptional_dest := NONE
      |>``);
  assert_parse_terminst("COMMINST @uvm.current_stack EXC (%n() %e())",
    ``CommInst [] CurrentStack <|
        normal_dest := (BlockLabel "n", []);
        exceptional_dest := SOME (BlockLabel "e", [])
      |> : ssavar terminst``);
    
Adam R. Nelson's avatar
Adam R. Nelson committed
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

(* Equality testing for basic blocks and functions is nigh-impossible, so
   instead just run the parsing functions and make sure they don't throw.
*)
val _ =
  print "parsing basic block\n";
  uir_block mock_context `
    %add(<int<8>> %a <int<8>> %b):
      %res = ADD <int<8>> %a %b
      RET (%res)
  `;

val _ =
  print "parsing function\n";
  uir_func mock_context (uir_funcsig mock_context `(int<8>) -> (int<8>)`) `
    %entry(<int<8>> %n):
      %is1 = ULE <int<8>> %n %one
      BRANCH2 %is1 %done() %recur(%n)
    %recur(<int<8>> %n):
      %minus1 = SUB <int<8>> %n %one
123
      %x = CALL <(int<8>) -> (int<8>)> %fact (%minus1) EXC (%mul(%n %x) %done())
Adam R. Nelson's avatar
Adam R. Nelson committed
124
125
126
127
128
129
130
131
132
    %mul(<int<8>> %m <int<8>> %n):
      %result = MUL <int<8>> %m %n
      RET (%result)
    %done():
      RET (%one)
  `;

val _ = export_theory()