src/clight/clightLustre.ml

   1
   2
   3 let f_expr set locals e sub_exprs_res =
   4   let e_res = match e with
   5     | Clight.Expr (Clight.Evar id, _) ->
   6       StringTools.Set.mem id set && not (List.mem id locals)
   7     | _ -> false in
   8   List.fold_left (||) false (e_res :: sub_exprs_res)
   9
  10 let f_stmt _ sub_exprs_res sub_stmts_res =
  11   List.fold_left (||) false (sub_exprs_res @ sub_stmts_res)
  12
  13 let references_stmt set locals stmt =
  14   ClightFold.statement2 (f_expr set locals) f_stmt stmt
  15
  16 let references_funct set (id, def) = match def with
  17   | Clight.Internal def ->
  18     let locals = List.map fst (def.Clight.fn_params @ def.Clight.fn_vars) in
  19     if references_stmt set locals def.Clight.fn_body then
  20       StringTools.Set.add id set
  21     else set
  22   | _ -> set
  23
  24 let references set p =
  25   List.fold_left references_funct set p.Clight.prog_funct
  26
  27
  28 let unsupported_functions p =
  29   let rec fixpoint set =
  30     let set' = references set p in
  31     if StringTools.Set.equal set set' then set
  32     else fixpoint set' in
  33   fixpoint (StringTools.Set.of_list ["calloc" ; "memcpy"])
  34
  35
  36 let remove_functions functions p =
  37   let f (id, _) = not (StringTools.Set.mem id functions) in
  38   let functs = List.filter f p.Clight.prog_funct in
  39   { p with Clight.prog_funct = functs }
  40
  41
  42 let simplify p =
  43   let unsupported = unsupported_functions p in
  44   remove_functions unsupported p