Project

General

Profile

« Previous | Next » 

Revision f6923c9e

Added by Pierre-Loïc Garoche over 10 years ago

Initial copy of the horn output version. Not really working yet

View differences:

src/c_backend.ml
819 819 
  let main_include, main_print, main_makefile =
820 820 
    match !Options.main_node with
821 821 
      | "" -> (fun _ -> ()), (fun _ -> ()), (fun _ -> ())
822 
      | main_node -> (
823 
	let main_node_opt =
824 
	  List.fold_left
825 
	  (fun res m ->
826 
	    match res with
827 
	      | Some _ -> res
828 
	      | None -> if m.mname.node_id = main_node then Some m else None)
829 
	  None machines
830 
      in
831 
      match main_node_opt with
822 
      | main_node -> (
823 
	match Machine_code.get_machine_opt main_node machines with
832 824 
	| None -> eprintf "Unable to find a main node named %s@.@?" main_node; (fun _ -> ()), (fun _ -> ()), (fun _ -> ())
833 825 
	| Some m -> print_main_header, print_main_fun machines m, print_makefile basename !Options.main_node
834 
    )
826 
      )
835 827 
  in
836 828 
  main_include source_fmt;
837 829 
  fprintf source_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h");
src/machine_code.ml
436 436 
  let nodes = get_nodes decls in
437 437 
   (* What to do with Imported/Sensor/Actuators ? *)
438 438 
   arrow_machine ::  List.map translate_decl nodes
439
439 

  		




  
  440
  
    
let get_machine_opt name machines =  


  		




  
  441
  
    
  List.fold_left 


  		




  
  442
  
    
    (fun res m -> 


  		




  
  443
  
    
      match res with 


  		




  
  444
  
    
      | Some _ -> res 


  		




  
  445
  
    
      | None -> if m.mname.node_id = name then Some m else None)


  		




  
  446
  
    
    None machines


  		




  
  447
  
    
    


  		




  440
  448
  
    

  		




  441
  449
  
    
(* Local Variables: *)


  		




  442
  450
  
    
(* compile-command:"make -C .." *)


  		












  

    
      src/main_lustre_compiler.ml
    
  





  216
  216
  
    

  		




  217
  217
  
    
  (* Printing code *)


  		




  218
  218
  
    
  let basename    = Filename.basename basename in


  		




  219
  
  
    
  if !Options.java then


  		




  220
  
  
    
    failwith "Sorry, but not yet supported !"


  		




  
  219
  
    
  let _ = match !Options.output with


  		




  
  220
  
    
      "C" -> 


  		




  
  221
  
    
	begin


  		




  
  222
  
    
	  let header_file = basename ^ ".h" in (* Could be changed *)


  		




  
  223
  
    
	  let source_file = basename ^ ".c" in (* Could be changed *)


  		




  
  224
  
    
	  let makefile_file = basename ^ ".makefile" in (* Could be changed *)


  		




  
  225
  
    
	  let spec_file_opt = if !Options.c_spec then 


  		




  
  226
  
    
	      (


  		




  
  227
  
    
		let spec_file = basename ^ "_spec.c" in


  		




  
  228
  
    
		report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s, %s and %s@,@?" header_file source_file spec_file);


  		




  
  229
  
    
		Some spec_file 


  		




  
  230
  
    
	      ) else (


  		




  
  231
  
    
		report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s and %s@,@?" header_file source_file);


  		




  
  232
  
    
		None 


  		




  
  233
  
    
	       )


  		




  
  234
  
    
	  in 


  		




  
  235
  
    
	  let header_out = open_out header_file in


  		




  
  236
  
    
	  let header_fmt = formatter_of_out_channel header_out in


  		




  
  237
  
    
	  let source_out = open_out source_file in


  		




  
  238
  
    
	  let source_fmt = formatter_of_out_channel source_out in


  		




  
  239
  
    
	  let makefile_out = open_out makefile_file in


  		




  
  240
  
    
	  let makefile_fmt = formatter_of_out_channel makefile_out in


  		




  
  241
  
    
	  let spec_fmt_opt = match spec_file_opt with


  		




  
  242
  
    
	      None -> None


  		




  
  243
  
    
	    | Some f -> Some (formatter_of_out_channel (open_out f))


  		




  
  244
  
    
	  in


  		




  
  245
  
    
	  report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");


  		




  
  246
  
    
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;


  		




  
  247
  
    
	end


  		




  
  248
  
    
    | "java" -> begin


  		




  
  249
  
    
      failwith "Sorry, but not yet supported !"


  		




  221
  250
  
    
    (*let source_file = basename ^ ".java" in


  		




  222
  251
  
    
      report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);


  		




  223
  252
  
    
      let source_out = open_out source_file in


  		




  224
  253
  
    
      let source_fmt = formatter_of_out_channel source_out in


  		




  225
  254
  
    
      report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");


  		




  226
  255
  
    
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)


  		




  227
  
  
    
  else begin


  		




  228
  
  
    
    let header_file = basename ^ ".h" in (* Could be changed *)


  		




  229
  
  
    
    let source_file = basename ^ ".c" in (* Could be changed *)


  		




  230
  
  
    
    let makefile_file = basename ^ ".makefile" in (* Could be changed *)


  		




  231
  
  
    
    let spec_file_opt = if !Options.c_spec then 


  		




  232
  
  
    
	(


  		




  233
  
  
    
	  let spec_file = basename ^ "_spec.c" in


  		




  234
  
  
    
	  report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s, %s and %s@,@?" header_file source_file spec_file);


  		




  235
  
  
    
	  Some spec_file 


  		




  236
  
  
    
	) else (


  		




  237
  
  
    
	  report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s and %s@,@?" header_file source_file);


  		




  238
  
  
    
	  None 


  		




  239
  
  
    
	 )


  		




  240
  
  
    
    in 


  		




  241
  
  
    
    let header_out = open_out header_file in


  		




  242
  
  
    
    let header_fmt = formatter_of_out_channel header_out in


  		




  243
  
  
    
    let source_out = open_out source_file in


  		




  244
  
  
    
    let source_fmt = formatter_of_out_channel source_out in


  		




  245
  
  
    
    let makefile_out = open_out makefile_file in


  		




  246
  
  
    
    let makefile_fmt = formatter_of_out_channel makefile_out in


  		




  247
  
  
    
    let spec_fmt_opt = match spec_file_opt with


  		




  248
  
  
    
	None -> None


  		




  249
  
  
    
      | Some f -> Some (formatter_of_out_channel (open_out f))


  		




  250
  
  
    
    in


  		




  251
  
  
    
    report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");


  		




  252
  
  
    
    C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;


  		




  253
  
  
    
  end;


  		




  
  256
  
    
    end


  		




  
  257
  
    
    | "horn" -> begin


  		




  
  258
  
    
      let fmt = Format.std_formatter in


  		




  
  259
  
    
      Horn_backend.translate fmt basename normalized_prog machine_code


  		




  
  260
  
    
    end


  		




  
  261
  
    
  in


  		




  254
  262
  
    
  report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");


  		




  255
  263
  
    
  (* We stop the process here *)


  		




  256
  264
  
    
  exit 0


  		












  

    
      src/options.ml
    
  





  30
  30
  
    
let ansi = ref false


  		




  31
  31
  
    
let check = ref false


  		




  32
  32
  
    
let c_spec = ref false


  		




  33
  
  
    
let java = ref false


  		




  
  33
  
    
let output = ref "C"


  		




  34
  34
  
    
let dest_dir = ref ""


  		




  35
  35
  
    
let verbose_level = ref 1


  		




  36
  36
  
    

  		




  ......




  44
  44
  
    
    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";


  		




  45
  45
  
    
    "-c-spec", Arg.Set c_spec, 


  		




  46
  46
  
    
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";


  		




  47
  
  
    
    "-java", Arg.Set java, "generates Java output instead of C";


  		




  
  47
  
    
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";


  		




  
  48
  
    
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";


  		




  48
  49
  
    
    "-print_types", Arg.Set print_types, "prints node types";


  		




  49
  50
  
    
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";


  		




  50
  51
  
    
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";


  		












Also available in:  Unified diff