Some refactoring

Adapted the parser/types/constructors for cocospec syntax

src/_tags.in

@@ -3,6 +3,9 @@ true: bin_annot, color(always)
 true: use_menhir
 
 # paths to sources
+"utils": include
+"checks": include
+"parsers": include
 "backends": include
 "backends/C": include
 "backends/Horn": include
@@ -41,7 +44,7 @@ true: use_menhir
 <**/test_json*.*>               : package(yojson)
 
 # Required for ocamldoc. Otherwise failed to build
-<*.ml{,i}>: package(ocamlgraph)
+<**/*.ml{,i}>: package(ocamlgraph)
 
 # Plugin dependencies
 @SALSA_TAG@

src/corelang.ml

@@ -165,10 +165,40 @@ let consts_of_enum_type top_decl =
 (*   Eexpr functions *)
 (************************************************************)
 
-let merge_contracts ann1 ann2 =
-  { requires = ann1.requires @ ann2.requires;
-    ensures = ann1.ensures @ ann2.ensures;
-    behaviors = ann1.behaviors @ ann2.behaviors;
+
+let empty_contract =
+  {
+    consts = []; locals = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
+  }
+    
+let mk_contract_var id is_const type_opt expr loc =
+  let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in
+  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
+  if is_const then
+  { empty_contract with consts = [v]; spec_loc = loc; }
+  else
+    { empty_contract with locals = [v]; spec_loc = loc; }
+
+let mk_contract_guarantees eexpr =
+  { empty_contract with guarantees = [eexpr]; spec_loc = eexpr.eexpr_loc }
+
+let mk_contract_assume eexpr =
+  { empty_contract with assume = [eexpr]; spec_loc = eexpr.eexpr_loc }
+
+let mk_contract_mode id rl el loc =
+  { empty_contract with modes = [{ mode_id = id; require = rl; ensure = el; mode_loc = loc; }]; spec_loc = loc }
+
+let mk_contract_import id ins outs loc =
+  { empty_contract with imports = [{import_nodeid = id; inputs = ins; outputs = outs; import_loc = loc; }]; spec_loc = loc }
+
+    
+let merge_contracts ann1 ann2 = (* keeping the first item loc *)
+  { consts = ann1.consts @ ann2.consts;
+    locals = ann1.locals @ ann2.locals;
+    assume = ann1.assume @ ann2.assume;
+    guarantees = ann1.guarantees @ ann2.guarantees;
+    modes = ann1.modes @ ann2.modes;
+    imports = ann1.imports @ ann2.imports;
     spec_loc = ann1.spec_loc
   }
 

src/corelang.mli

@@ -156,6 +156,12 @@ val copy_prog: top_decl list -> top_decl list
 
 (** Annotation expression related functions *)
 val mkeexpr: Location.t ->  expr -> eexpr
+val empty_contract: contract_desc
+val mk_contract_var: ident -> bool -> type_dec option -> expr -> Location.t -> contract_desc
+val mk_contract_guarantees: eexpr -> contract_desc
+val mk_contract_assume: eexpr -> contract_desc
+val mk_contract_mode: ident -> eexpr list -> eexpr list -> Location.t -> contract_desc
+val mk_contract_import: ident -> expr list -> expr list -> Location.t -> contract_desc
 val merge_contracts:  contract_desc -> contract_desc -> contract_desc 
 val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
 val update_expr_annot: ident -> expr -> expr_annot -> expr
@@ -170,6 +176,8 @@ val mk_fresh_var: node_desc -> Location.t -> Types.type_expr ->  Clocks.clock_ex
 val get_expr_calls: top_decl list -> expr -> Utils.ISet.t
 
 val eq_has_arrows: eq -> bool
+
+
 (* Local Variables: *)
 (* compile-command:"make -C .." *)
 (* End: *)

src/inliner.ml

@@ -421,12 +421,8 @@ let witness filename main_name orig inlined type_env clock_env =
     node_dec_stateless = false;
     node_stateless = None;
     node_spec = Some 
-      {requires = []; 
-       ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];
-       behaviors = [];
-       spec_loc = loc
-      };
-    node_annot = [];
+      (mk_contract_guarantees (mkeexpr loc (mkexpr loc (Expr_ident ok_ident))));
+      node_annot = [];
   }
   in
   let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in

src/lustre_types.ml

@@ -52,6 +52,7 @@ type constant =
   | Const_array of constant list
   | Const_tag of label
   | Const_string of string (* used only for annotations *)
+  | Const_modeid of string (* used only for annotations *)
   | Const_struct of (label * constant) list
 
 type quantifier_type = Exists | Forall
@@ -124,18 +125,27 @@ and expr_annot =
  {annots: (string list * eexpr) list;
   annot_loc: Location.t}
 
-type contract_desc = {
+type contract_mode =
+  { mode_id: ident; require: eexpr list; ensure: eexpr list; mode_loc: Location.t}
+
+type contract_import =
+  { import_nodeid: ident; inputs: expr list; outputs: expr list; import_loc: Location.t }
+    
+type contract_desc = 
+  {
 (* TODO: 
    local variables 
    rename: assume/guarantee
            in behavior mode (id, requires/ensures)
    import contract
 *)
-  
-  requires: eexpr list;
-  ensures: eexpr list;
-  behaviors: (string * eexpr list * eexpr list * Location.t) list;
-  spec_loc: Location.t;
+       consts: var_decl list;
+       locals: var_decl list;
+       assume: eexpr list;
+       guarantees: eexpr list;
+       modes: contract_mode list;
+       imports: contract_import list; 
+       spec_loc: Location.t;
 }
 
 type offset =

src/normalization.ml

@@ -460,12 +460,12 @@ let normalize_eexpr decls node vars ee =
     
 let normalize_spec decls node vars s =
   let nee = normalize_eexpr decls node vars in
-  List.iter nee s.requires;
-  List.iter nee s.ensures;
-  List.iter (fun (_, assumes, ensures, _) -> 
-      List.iter nee assumes;
-    List.iter nee ensures
-  ) s.behaviors
+  List.iter nee s.assume;
+  List.iter nee s.guarantees;
+  List.iter (fun m -> 
+      List.iter nee m.require;
+    List.iter nee m.ensure
+  ) s.modes
   
     
 (* The normalization phase introduces new local variables

src/lexerLustreSpec.mll → src/parsers/lexerLustreSpec.mll

@@ -55,12 +55,13 @@ let keyword_table =
   "const", CONST;
   (* "include", INCLUDE; *)
   "assert", ASSERT;
-  "ensures", ENSURES;
-  "requires", REQUIRES;
-  "observer", OBSERVER;
+  "ensure", ENSURE;
+  "require", REQUIRE;
+  (* "observer", OBSERVER; *)
   "invariant", INVARIANT;
-  "behavior", BEHAVIOR;
-  "assumes", ASSUMES;
+  "mode", MODE;
+  "assume", ASSUME;
+  "guarantees", GUARANTEES;
   "exists", EXISTS;
   "forall", FORALL;
   "c_code", CCODE;

src/parserLustreSpec.mly → src/parsers/parserLustreSpec.mly

@@ -84,24 +84,25 @@ lustre_spec:
 | contract EOF { $1 }
 
 contract:
-requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; } }
- 
-requires:
 { [] }
-| REQUIRES qexpr SCOL requires { $2::$4 }
-
-ensures:
-{ [] }
-| ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 }
-| OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
-
-behaviors:
-{ [] }
-| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5)::$6 }
-
-assumes:
+| CONST ident EQ expr SCOL contract
+    { Const($2, None, $4)::$3 }
+| CONST ident COL typeconst EQ expr SCOL contract
+    { Const($2, Some($4), $6)::$3 }
+| ASSUME qexpr SCOL contract
+    { Assume($2)::$4 }
+| GUARANTEES qexpr SCOL contract	
+    { Guarantees($2)::$4 }
+| MODE ident LPAR mode_content RPAR SCOL contract
+    { Mode($2,$4)::$7 }	
+| IMPORT ident LPAR tuple_expr RPAR returns LPAR tuple_expr RPAR SCOL contract
+    { Import($2, $4, $8)::$11 }
+	
+
+mode_content:
 { [] }
-| ASSUMES qexpr SCOL assumes { $2::$4 } 
+| REQUIRE qexpr COL mode_content { Require($2)::$4 }
+| ENSURE qexpr COL mode_content { Require($2)::$4 }
 
 tuple_qexpr:
 | qexpr COMMA qexpr {[$3;$1]}

src/parser_lustre.mly → src/parsers/parser_lustre.mly

@@ -75,8 +75,8 @@ let rec fby expr n init =
 %token MULT DIV MOD
 %token MINUS PLUS UMINUS
 %token PRE ARROW
-%token REQUIRES ENSURES OBSERVER
-%token INVARIANT BEHAVIOR ASSUMES CCODE MATLAB
+%token REQUIRE ENSURE ASSUME GUARANTEES IMPORT
+%token INVARIANT MODE CCODE MATLAB
 %token EXISTS FORALL
 %token PROTOTYPE LIB
 %token EOF
@@ -214,30 +214,30 @@ in_lib_list:
 
 top_decl:
 | CONST cdecl_list { List.rev ($2 false) }
-| nodespec_list state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL 
+| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespec_list locals LET stmt_list TEL 
     {
      let stmts, asserts, annots = $16 in
       (* Declaring eqs annots *)
       List.iter (fun ann -> 
 	List.iter (fun (key, _) -> 
-	  Annotations.add_node_ann $3 key
+	  Annotations.add_node_ann $2 key
 	) ann.annots
       ) annots;
      (* Building the node *)
      let nd = mktop_decl false (Node
-				  {node_id = $3;
+				  {node_id = $2;
 				   node_type = Types.new_var ();
 				   node_clock = Clocks.new_var true;
-				   node_inputs = List.rev $5;
-				   node_outputs = List.rev $10;
+				   node_inputs = List.rev $4;
+				   node_outputs = List.rev $9;
 				   node_locals = List.rev $14;
 				   node_gencalls = [];
 				   node_checks = [];
 				   node_asserts = asserts; 
 				   node_stmts = stmts;
-				   node_dec_stateless = $2;
+				   node_dec_stateless = $1;
 				   node_stateless = None;
-				   node_spec = $1;
+				   node_spec = $13;
 				   node_annot = annots})
      in
      pop_node ();
@@ -330,26 +330,31 @@ lustre_spec:
 | contract EOF { $1 }
 
 contract:
-requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
- 
-requires:
-{ [] }
-| REQUIRES qexpr SCOL requires { $2::$4 }
-
-ensures:
-{ [] }
-| ENSURES qexpr SCOL ensures { $2 :: $4 }
-| OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { 
-  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
-}
-
-behaviors:
-{ [] }
-| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
-
-assumes:
-{ [] }
-| ASSUMES qexpr SCOL assumes { $2::$4 } 
+{ empty_contract }
+| CONST IDENT EQ expr SCOL contract
+    { merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
+| CONST IDENT COL typeconst EQ expr SCOL contract
+    { merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
+| VAR IDENT EQ expr SCOL contract
+    { merge_contracts (mk_contract_var $2 false None $4 (get_loc())) $6 }
+| VAR IDENT COL typeconst EQ expr SCOL contract
+    { merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
+| ASSUME qexpr SCOL contract
+    { merge_contracts (mk_contract_assume $2) $4 }
+| GUARANTEES qexpr SCOL contract	
+    { merge_contracts (mk_contract_guarantees $2) $4 }
+| MODE IDENT LPAR mode_content RPAR SCOL contract
+	{ merge_contracts (
+	  let r, e = $4 in 
+	  mk_contract_mode $2 r e (get_loc())) $7 }	
+| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract
+    { merge_contracts (mk_contract_import $2  $4  $8 (get_loc())) $11 }
+	
+
+mode_content:
+{ [], [] }
+| REQUIRE qexpr SCOL mode_content { let (r,e) = $4 in $2::r, e }
+| ENSURE qexpr SCOL mode_content { let (r,e) = $4 in r, $2::e }
 
 /* WARNING: UNUSED RULES */
 tuple_qexpr:
@@ -381,7 +386,8 @@ expr:
   INT {mkexpr (Expr_const (Const_int $1))}
 | REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
 | STRING {mkexpr (Expr_const (Const_string $1))}
-
+| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))} 
+    
 /* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
 /* Idents or type enum tags */
 | IDENT { mkexpr (Expr_ident $1) }
@@ -645,7 +651,7 @@ lustre_annot_list:
 | kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
 | IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
 | INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
-| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
+// (* | OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } *)
 | CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 }
 | MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 }
 

src/printers.ml

@@ -288,14 +288,28 @@ let pp_eexpr fmt e =
 
 let pp_spec fmt spec =
   fprintf fmt "@[<hov 2>(*@@ ";
-  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
-  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
-  fprintf_list ~sep:"@," (fun fmt (name, assumes, ensures, _) -> 
-    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
-      name
-      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
-      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures
-  ) fmt spec.behaviors;
+  (* const are prefixed with const in pp_var and with nothing for regular
+     variables. We adapt the call to produce the appropriate output. *)
+  fprintf_list ~sep:"@,@@ " (fun fmt v ->
+    fprintf fmt "%s%a = %t;"
+      (if v.var_dec_const then "" else "var")
+      pp_var v
+      (fun fmt -> match v.var_dec_value with None -> () | Some e -> pp_expr fmt e)
+  ) fmt (spec.consts @ spec.locals);
+  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
+  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
+  fprintf_list ~sep:"@,@@ " (fun fmt mode ->
+    fprintf fmt "mode %s (@[@ %a@ %a@]);" 
+      mode.mode_id
+      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
+      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
+  ) fmt spec.modes;
+  fprintf_list ~sep:"@,@@ " (fun fmt import ->
+    fprintf fmt "import %s (%a) returns (%a);" 
+      import.import_nodeid
+      (fprintf_list ~sep:"@ " pp_expr) import.inputs
+      (fprintf_list ~sep:"@ " pp_expr) import.outputs
+  ) fmt spec.imports;
   fprintf fmt "@]*)";
   ()