blob: 09c8b86b388d71934e4c03316d10075c6164ffc2 (
plain) (
blame)
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
open Xi_lib
open Ast
open Types
module AllExpressionsAreTypecheck = struct
exception MissingTypeInformation of location
module Implementation(M:sig val node2type: (node_tag, normal_type) Hashtbl.t end) = struct
open M
let check_tag loc tag =
match Hashtbl.find_opt node2type tag with
| Some _ -> ()
| None -> raise (MissingTypeInformation loc)
let expr_subexpressions = function
| EXPR_Id _ -> []
| EXPR_Int _ -> []
| EXPR_Char _ -> []
| EXPR_String _ -> []
| EXPR_Bool _ -> []
| EXPR_Relation {lhs; rhs; _} ->
[lhs; rhs]
| EXPR_Binop {lhs; rhs; _} ->
[lhs; rhs]
| EXPR_Length {arg; _} ->
[arg]
| EXPR_Unop {sub; _} ->
[sub]
| EXPR_Call (Call {arguments; _}) ->
arguments
| EXPR_Index {expr; index; _} ->
[expr; index]
| EXPR_Struct {elements; _} ->
elements
let some2list = function
| Some x -> [x]
| None -> []
let block_substatements = function
| STMTBlock {body; _} -> body
let block_substatements_opt = function
| Some (STMTBlock {body; _}) -> body
| None -> []
let stmt_subexpressions = function
| STMT_Call (Call {arguments; _}) ->
arguments
| STMT_Assign {rhs; _} ->
[rhs]
| STMT_VarDecl {init=Some init; _} ->
[init]
| STMT_VarDecl {init=None; _} ->
[]
| STMT_If {cond; _} ->
[cond]
| STMT_While {cond; _} ->
[cond]
| STMT_Return {values; _} ->
values
| STMT_MultiVarDecl {init=Call{arguments; _}; _} ->
arguments
| STMT_Block _ ->
[]
let stmt_substatements = function
| STMT_Call _ ->
[]
| STMT_Assign _ ->
[]
| STMT_VarDecl _ ->
[]
| STMT_If {then_branch; else_branch; _} ->
[then_branch] @ some2list else_branch
| STMT_While {body; _} ->
[body]
| STMT_Return _ ->
[]
| STMT_MultiVarDecl _ ->
[]
| STMT_Block block ->
block_substatements block
let rec verify_expression e =
check_tag (location_of_expression e) (tag_of_expression e);
let sube = expr_subexpressions e in
List.iter verify_expression sube
let rec verify_statement s =
let exprs = stmt_subexpressions s in
let stmts = stmt_substatements s in
List.iter verify_expression exprs;
List.iter verify_statement stmts
let verify_block_opt s =
let stmts = block_substatements_opt s in
List.iter verify_statement stmts
let verify_global_declaration = function
| GDECL_Function {body; _} ->
verify_block_opt body
let verify_module_definition (ModuleDefinition {global_declarations}) =
List.iter verify_global_declaration global_declarations
end
let verify_module_definition node2tag mdef =
try
let module Instance = Implementation(struct let node2type = node2tag end) in
Instance.verify_module_definition mdef;
true
with MissingTypeInformation e ->
Format.eprintf "Missing type information for expression %s\n%!" (string_of_location e);
false
end
|
