Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / C / c_backend_spec.ml @ 5fccce23

History | View | Annotate | Download (8.19 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Format
13
open Lustre_types
14
open Machine_code
15
open C_backend_common
16
open Utils
17

    
18
(**************************************************************************)
19
(*     Printing spec for c *)
20

    
21
(**************************************************************************)
22
(* OLD STUFF ???
23

    
24

    
25
let pp_acsl_type var fmt t =
26
  let rec aux t pp_suffix =
27
  match (Types.repr t).Types.tdesc with
28
  | Types.Tclock t'       -> aux t' pp_suffix
29
  | Types.Tbool           -> fprintf fmt "int %s%a" var pp_suffix ()
30
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
31
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
32
  | Types.Tarray (d, t')  ->
33
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
34
    aux t' pp_suffix'
35
  (* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)
36
  (* | Types.Tconst ty       -> fprintf fmt "%s %s" ty var *)
37
  (* | Types.Tarrow (_, _)   -> fprintf fmt "void (\*%s)()" var *)
38
  | _                     -> eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false
39
  in aux t (fun fmt () -> ())
40

    
41
let pp_acsl_var_decl fmt id =
42
  pp_acsl_type id.var_id fmt id.var_type
43

    
44

    
45
let rec pp_eexpr is_output fmt eexpr = 
46
  let pp_eexpr = pp_eexpr is_output in
47
  match eexpr.eexpr_desc with
48
    | EExpr_const c -> Printers.pp_econst fmt c
49
    | EExpr_ident id -> 
50
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
51
    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
52
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
53
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
54
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
55
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
56
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
57
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
58
    | EExpr_merge (id, e1, e2) -> 
59
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
60
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
61
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e 
62
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e 
63

    
64

    
65
    (* | EExpr_whennot _ *)
66
    (* | EExpr_uclock _ *)
67
    (* | EExpr_dclock _ *)
68
    (* | EExpr_phclock _ -> assert false *)
69
and pp_eapp is_output fmt id e r =
70
  let pp_eexpr = pp_eexpr is_output in
71
  match r with
72
  | None ->
73
    (match id, e.eexpr_desc with
74
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
75
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
76
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
77
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
78
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
79
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
80
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
81
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
82
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
83
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
84
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
85
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
86
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
87
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
88
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
89
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
90
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
91
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
92
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
93
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
94

    
95
let pp_ensures is_output fmt e =
96
  match e with
97
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e
98
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args
99

    
100
let pp_acsl_spec outputs fmt spec =
101
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
102
  let pp_eexpr = pp_eexpr is_output in
103
  fprintf fmt "@[<v 2>/*@@ ";
104
  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
105
  Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
106
  fprintf fmt "@ ";
107
  (* fprintf fmt "assigns *self%t%a;@ "  *)
108
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
109
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
110
  Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
111
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
112
      name
113
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
114
      (Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
115
  ) fmt spec.behaviors;
116
  fprintf fmt "@]@ */@.";
117
  ()
118

    
119

    
120

    
121

    
122
let print_machine_decl_prefix fmt m =
123
   (* Print specification if any *)
124
   (match m.mspec with
125
  | None -> ()
126
  | Some spec -> 
127
    pp_acsl_spec m.mstep.step_outputs fmt spec
128
  )
129

    
130
  *)
131

    
132
(**************************************************************************)
133
(*                              MAKEFILE                                  *)
134
(**************************************************************************)
135

    
136
let makefile_targets fmt basename nodename dependencies =
137
  fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
138
  (* EACSL version of library file . c *)
139
  fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
140
  fprintf fmt 
141
    "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@." 
142
    basename basename; 
143
  fprintf fmt "@.";
144
  fprintf fmt "@.";
145

    
146
  (* EACSL version of library file . c + main .c  *)
147
  fprintf fmt "%s_main_eacsl.c: %s.c %s.h %s_main.c@." basename basename basename basename;
148
  fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_main.c -then-on e-acsl -print -ocode %s_main_eacsl.i@." 
149
    basename basename basename; 
150
  (* Ugly hack to deal with eacsl bugs *)
151
  fprintf fmt "\tgrep -v _fc_stdout %s_main_eacsl.i > %s_main_eacsl.c" basename basename;
152
  fprintf fmt "@.";
153
  fprintf fmt "@.";
154

    
155
  (* EACSL version of binary *)
156
  fprintf fmt "%s_main_eacsl: %s_main_eacsl.c@." basename basename;
157
  fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_main_eacsl.c@." basename; (* compiling instrumented lib + main *)
158
  C_backend_makefile.fprintf_dependencies fmt dependencies; 
159
  fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@." 
160
    basename 
161
    (Utils.fprintf_list ~sep:" " (fun fmt dep -> Format.fprintf fmt "%s.o" dep.name)) 
162
    (C_backend_makefile.compiled_dependencies dependencies)
163
    ("${FRAMACEACSL}/e_acsl.c " 
164
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " 
165
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
166
    basename 
167
    (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) 
168
    (C_backend_makefile.lib_dependencies dependencies)
169
  ;
170
  fprintf fmt "@.";
171

    
172
module MakefileMod =
173
struct
174
  let other_targets = makefile_targets
175
    
176
end
177

    
178
(* Local Variables: *)
179
(* compile-command:"make -C ../../.." *)
180
(* End: *)