Project

General

Profile

Revision 0d54d8a8

View differences:

TODO.org
131 131
  - in lustre file: contract attached to lustre node before the locals/let
132 132
  - in lusi file: contract attached to lustre node before the node foo ...
133 133

  
134
- Dev. choices
135
  - contracts rely look like imported node: a signature and a contract content attached
136
    - in lusi one could have an alias for contract / imported node
137
    - in lus similarly a top level contract could be parsed as an imported node
138
    - contract import would amount to concatenate contract elements
139
      from provided nodes or imported nodes.
140

  
134 141
** Development
135 142
*** Done
136 143
- (ploc) retirer le parser Kind2 et revenir à celui de lustrec
......
150 157
  - EMF
151 158
  - LustreV
152 159

  
160
* Slicing
161
  - reprendre le slicing inlined de seal pour
162
  - when provided with a main node and a selection of outputs or memories
163
    - slice the local node
164
    - for each node called try to slice to the selected vars
165
  - could be used to analyze counterexamples
153 166
* TODO refactoring + doc
154 167
- separate lustre types from machine types in different files
155 168
- split basic libs into backend specific files
src/backends/C/c_backend_common.ml
231 231
    | Const_tag t     -> pp_c_tag fmt t
232 232
    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
233 233
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
234
    | Const_string _ -> assert false (* string occurs in annotations not in C *)
234
    | Const_string _ | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
235 235

  
236 236
       
237 237
(* Prints a value expression [v], with internal function calls only.
src/backends/C/c_backend_src.ml
137 137
    | Const_array ca       -> let var_type = Types.array_element_type var_type in
138 138
                              fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_c_const_suffix var_type)) ca
139 139
    | Const_struct fl       -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)) fl
140
    | Const_string _        -> assert false (* string occurs in annotations not in C *)
140
    | Const_string _
141
      | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
141 142

  
142 143

  
143 144
(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
src/backends/Horn/horn_backend_traces.ml
112 112
              (fun def ->
113 113
                match def with
114 114
                | Eq eq -> (match eq.eq_lhs with
115
                            | [v] -> v = var_id 
115
                            | [v] -> v = var_id
116
                            | _ -> assert false
116 117
                           )
117 118
                | _ -> false)
118 119
              m.mname.node_stmts
src/checks/algebraicLoop.ml
143 143
  Options.verbose_level := !Options.verbose_level - 2;
144 144

  
145 145
  (* Mini stage 1 *)
146
  (* Extracting dependencies *)
147
  let dependencies = Compiler_common.import_dependencies prog in
146
  (* Extracting dependencies: fill some table with typing info *)
147
  ignore (Compiler_common.import_dependencies prog);
148 148
  (* Local inlining *)
149 149
  let prog = Inliner.local_inline prog (* type_env clock_env *) in
150 150
  (* Checking stateless/stateful status *)
src/clock_calculus.ml
734 734
  nd.nodei_clock <- ck_node;
735 735
  Env.add_value env nd.nodei_id ck_node
736 736

  
737

  
738
let new_env = clock_var_decl_list
739
              
737 740
let clock_top_const env cdecl=
738 741
  let ck = new_var false in
739 742
  try_generalize ck cdecl.const_loc;
src/lustre_types.ml
148 148
       spec_loc: Location.t;
149 149
}
150 150

  
151

  
151 152
type offset =
152 153
| Index of Dimension.dim_expr
153 154
| Field of label
......
214 215
     mutable const_type: Types.type_expr;
215 216
    }
216 217

  
218
  
217 219
type top_decl_desc =
218 220
| Node of node_desc
219 221
| Const of const_desc
......
221 223
| Open of bool * string (* the boolean set to true denotes a local
222 224
			   lusi vs a lusi installed at system level *)
223 225
| TypeDef of typedef_desc
224
| Contract of contract_desc
225 226
    
226 227
type top_decl =
227 228
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
src/mpfr.ml
211 211
  let norm_eq = { eq with eq_rhs = norm_rhs } in
212 212
  norm_eq::defs', vars'
213 213

  
214
(* let inject_eexpr ee =
215
 *   { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }
216
 *   
217
 * let inject_spec s =
218
 *   { s with
219
 *     assume = List.map inject_eexpr s.assume;
220
 *     guarantees = List.map inject_eexpr s.guarantees;
221
 *     modes = List.map (fun m ->
222
 *                 { m with
223
 *                   require = List.map inject_eexpr m.require;
224
 *                   ensure = List.map inject_eexpr m.ensure
225
 *                 }
226
 *               ) s.modes
227
 *   } *)
228
  
214 229
(** normalize_node node returns a normalized node, 
215 230
    ie. 
216 231
    - updated locals
......
247 262
     - compute the associated expression without aliases     
248 263
  *)
249 264
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
265
  (* See comment below
266
   *  let spec = match node.node_spec with
267
   *   | None -> None
268
   *   | Some spec -> Some (inject_spec spec)
269
   * in *)
250 270
  let node =
251 271
  { node with 
252 272
    node_locals = new_locals; 
253 273
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
274
    (* Incomplete work: TODO. Do we have to inject MPFR code here?
275
       Does it make sense for annotations? For me, only if we produce
276
       C code for annotations. Otherwise the various verification
277
       backend should have their own understanding, but would not
278
       necessarily require this additional normalization. *)
279
    (* 
280
       node_spec = spec;
281
       node_annot = List.map (fun ann -> {ann with
282
           annots = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots}
283
         ) node.node_annot *)
254 284
  }
255 285
  in ((*Printers.pp_node Format.err_formatter node;*) node)
256 286

  
src/mutation.ml
223 223
  | Const_real (n, i, s) -> let (n', i', s') = rdm_mutate_real (n, i, s) in Const_real (n', i', s')
224 224
  | Const_array _
225 225
  | Const_string _
226
  | Const_modeid _
226 227
  | Const_struct _
227 228
  | Const_tag _ -> c
228 229

  
src/normalization.ml
488 488
let normalize_node decls node =
489 489
  reset_cpt_fresh ();
490 490
  let inputs_outputs = node.node_inputs@node.node_outputs in
491
  let is_local v =
492
    List.for_all ((<>) v) inputs_outputs in
493 491
  let orig_vars = inputs_outputs@node.node_locals in
494 492
  let not_is_orig_var v =
495 493
    List.for_all ((!=) v) orig_vars in
......
595 593
    end;
596 594
  
597 595
 
598
 let new_locals = List.filter is_local vars in (* TODO a quoi ca sert ? *)
599 596
  let node =
600 597
    { node with
601 598
      node_locals = all_locals;
src/printers.ml
367 367
  | Const c -> fprintf fmt "const %a" pp_const_decl c
368 368
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
369 369
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
370
  | Contract c -> pp_spec fmt c (* TODO: may be we need to produce it outside of comments.To be discussed *)
371 370
  
372 371
let pp_prog fmt prog =
373 372
  (* we first print types: the function SortProg.sort could do the job but ut
......
385 384
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
386 385
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
387 386
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
388
  | Contract c -> fprintf fmt "(*@ contract *)@ "
389

  
387
  
390 388
let pp_lusi fmt decl = 
391 389
  match decl.top_decl_desc with
392 390
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
......
394 392
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
395 393
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
396 394
  | Node _ -> assert false
397
  | Contract c -> pp_spec fmt c (* TODO idem pp_node: how to print contract in lusi, within/without comments brackets ? *)
398 395
                
399 396
let pp_lusi_header fmt basename prog =
400 397
  fprintf fmt "@[<v 0>";
src/typing.ml
767 767
         type_top_const env c
768 768
      | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
769 769
      | Open _  -> env
770
      | Contract c -> type_spec env c
771

  
770
    
772 771
    let get_type_of_call decl =
773 772
      match decl.top_decl_desc with
774 773
      | Node nd         ->
......
812 811
         uneval_node_generics (nd.node_inputs @ nd.node_outputs)
813 812
      | ImportedNode nd ->
814 813
         uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
815
      | Contract c -> uneval_spec_generics c
816 814
      | Const _
817 815
        | TypeDef _
818 816
        | Open _

Also available in: Unified diff