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

Last change on this file was 740, checked in by ayache, 9 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.