source: Deliverables/D2.2/8051/src/cminor/cminorPointers.ml @ 740

Last change on this file since 740 was 740, checked in by ayache, 10 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 6.5 KB
Line 
1
2let union_list =
3  List.fold_left StringTools.Set.union StringTools.Set.empty
4
5
6(** [is_pointer ptrs e] returns true only if the expression [e] represents an
7    address when considering that the variables in the set [ptrs] are
8    pointers. *)
9
10let rec is_pointer ptrs = function
11  | Cminor.Id x -> StringTools.Set.mem x ptrs
12  | Cminor.Cst (AST.Cst_stackoffset _) | Cminor.Cst (AST.Cst_addrsymbol _) ->
13    true
14  | Cminor.Op1 (AST.Op_id, e) -> is_pointer ptrs e
15  | Cminor.Op1 (AST.Op_ptrofint, _) -> true
16  | Cminor.Op2 (AST.Op_addp, _, _) | Cminor.Op2 (AST.Op_subp, _, _) -> true
17  | Cminor.Cond (_, e2, e3) -> (is_pointer ptrs e2) || (is_pointer ptrs e3)
18  | Cminor.Exp_cost (_, e) -> is_pointer ptrs e
19  | _ -> false
20
21(** [is_op1_pointer op1] returns true iff [op1] returns a pointer. *)
22
23let is_op1_pointer = function
24  | AST.Op_intofptr -> true
25  | _ -> false
26
27(** When [op2_ptr_args op2 = (b1, b2)] [b1] (resp. [b2]) is true iff the first
28    (resp. second) argument of [op2] must be a pointer. *)
29
30let op2_ptr_args = function
31  | AST.Op_cmpp _ -> (true, true)
32  | AST.Op_addp | AST.Op_subp -> (true, false)
33  | _ -> (false, false)
34
35(** [expression_pointer is_pointer e] returns the set of variables that
36    represent an address in the expression [e]. The [is_pointer] function is a
37    predicate telling whether or not a given variable is a pointer. *)
38
39let rec expression_pointers is_pointer = function
40  | Cminor.Id x when is_pointer -> StringTools.Set.singleton x
41  | Cminor.Id x -> StringTools.Set.empty
42  | Cminor.Cst _ -> StringTools.Set.empty
43  | Cminor.Exp_cost (_, e)
44  | Cminor.Op1 (AST.Op_id, e) -> expression_pointers is_pointer e
45  | Cminor.Op1 (op1, e) -> expression_pointers (is_op1_pointer op1) e
46  | Cminor.Op2 (op2, e1, e2) ->
47    let (b1, b2) = op2_ptr_args op2 in
48    let res1 = expression_pointers b1 e1 in
49    let res2 = expression_pointers b2 e2 in
50    union_list [res1 ; res2]
51  | Cminor.Mem (_, e) -> expression_pointers true e
52  | Cminor.Cond (e1, e2, e3) ->
53    let res1 = expression_pointers false e1 in
54    let res2 = expression_pointers is_pointer e2 in
55    let res3 = expression_pointers is_pointer e3 in
56    union_list [res1 ; res2 ; res3]
57
58
59(** [f_statement_pointers ret_type ptrs stmt subexp_res substmt_res] returns the
60    set of variables that are pointers in [stmt]. [ret_type] is the type of the
61    returned expression of the statement, if any. [ptrs] is a set of already
62    known pointer variables. [subexp_res] is not used. [substmt_res] is the
63    result of the application of the function on the sub-statements of
64    [stmt]. *)
65
66let f_statement_pointers ret_type ptrs stmt _ substmt_res =
67  let ptrs = union_list (ptrs :: substmt_res) in
68  let stmt_ptrs = match stmt with
69    | Cminor.St_assign (x, e) ->
70      let res1 =
71        if is_pointer ptrs e then StringTools.Set.singleton x
72        else StringTools.Set.empty in
73      let res2 = expression_pointers (StringTools.Set.mem x ptrs) e in
74      union_list [res1 ; res2]
75    | Cminor.St_store (_, e1, e2) ->
76      let res1 =
77        expression_pointers
78          true (* when storing, [e1] must be an address *) e1 in
79      let res2 = expression_pointers false e2 in
80      union_list [res1 ; res2]
81    | Cminor.St_call (None, f, args, sg)
82    | Cminor.St_tailcall (f, args, sg) ->
83      let res1 =
84        expression_pointers
85          true (* when calling, [f] must be an address *) f in
86      (* Fetch the results on the arguments of the function. *)
87      let f typ e = expression_pointers (typ = AST.Sig_ptr) e in
88      let res2 = union_list (List.map2 f sg.AST.args args) in
89      union_list [res1 ; res2]
90    | Cminor.St_call (Some x, f, args, sg) ->
91      let res1 =
92        if sg.AST.res = AST.Type_ret AST.Sig_ptr then
93          StringTools.Set.singleton x
94        else StringTools.Set.empty in
95      let res2 = expression_pointers true f in
96      let f typ e = expression_pointers (typ = AST.Sig_ptr) e in
97      let res3 = union_list (List.map2 f sg.AST.args args) in
98      union_list [res1 ; res2 ; res3]
99    | Cminor.St_ifthenelse (e, _, _) -> expression_pointers false e
100    | Cminor.St_return (Some e) ->
101      expression_pointers (ret_type = AST.Type_ret AST.Sig_ptr) e
102    | _ -> StringTools.Set.empty
103  in
104  union_list [ptrs ; stmt_ptrs]
105
106(** [statement_pointers type_ret stmt ptrs] is one iteration that collects the
107    pointers of [stmt]. [type_ret] is the type of the returned expression of the
108    statement, if any. [ptrs] is a set of already known pointer variables.  *)
109
110let statement_pointers ret_type stmt ptrs =
111  CminorFold.statement_left (fun _ _ -> StringTools.Set.empty)
112    (f_statement_pointers ret_type ptrs) stmt
113
114
115(** [init_pointer def] returns the local variables or parameters of a function
116    that can be deduced as pointers from the signature and the declarations of
117    the function. *)
118
119let init_pointers def =
120  let ptrs = StringTools.Set.empty in
121  (* Adding the parameter pointers. *)
122  let f ptrs x = function
123    | AST.Sig_ptr -> StringTools.Set.add x ptrs
124    | _ -> ptrs in
125  let ptrs =
126    List.fold_left2 f ptrs def.Cminor.f_params def.Cminor.f_sig.AST.args in
127  (* Adding the local pointers. *)
128  let f ptrs x =
129    if List.mem x def.Cminor.f_ptrs then StringTools.Set.add x ptrs
130    else
131      if StringTools.Set.mem x ptrs then
132        (* Case where a parameter with the same name is a pointer. Thus, for the
133           moment, it is in [ptrs]. But only the local can be seen inside the
134           function and it is not a pointer, so we have to remove it. *)
135        StringTools.Set.remove x ptrs
136      else ptrs in
137  List.fold_left f ptrs def.Cminor.f_vars
138
139
140(* A function that iterates another function until a fixpoint is reached. The
141   result is a set of strings. *)
142
143let rec fixpoint f s =
144  let s' = f s in
145  if StringTools.Set.equal s s' then s
146  else fixpoint f s'
147
148
149let internal_pointers def =
150  (* The pointers of a function are found by iterating one step of collecting
151     the pointers until a fixpoint is reached. *)
152  let ptrs = init_pointers def in
153  let ptrs =
154    fixpoint
155      (statement_pointers def.Cminor.f_sig.AST.res def.Cminor.f_body) ptrs in
156  let ptrs = StringTools.Set.fold (fun x l -> x :: l) ptrs [] in
157  { def with Cminor.f_ptrs = ptrs }
158
159let fun_def_pointers (id, def) =
160  let def' = match def with
161    | Cminor.F_int def -> Cminor.F_int (internal_pointers def)
162    | _ -> def
163  in
164  (id, def')
165
166(** [fill p] sets the pointer variables field of each function of the program
167    [p]. The algorithm works as a fixpoint: initially, there are no pointers,
168    then we collect the pointers found in one pass and repeat the operation
169    considering the new result. *)
170
171let fill p =
172  { p with Cminor.functs = List.map fun_def_pointers p.Cminor.functs }
Note: See TracBrowser for help on using the repository browser.