[kernel/logic] cil printer with module names

src/kernel_services/ast_printing/cil_printer.ml

@@ -1263,9 +1263,9 @@ class cil_printer () = object (self)
   method builtin_logic_info fmt bli =
     fprintf fmt "%a" self#varname bli.bl_name
 
-  method logic_type_info fmt s = fprintf fmt "%a" self#varname s.lt_name
+  method logic_type_info fmt s = fprintf fmt "%a" self#logic_name s.lt_name
 
-  method logic_ctor_info fmt ci =  fprintf fmt "%a" self#varname ci.ctor_name
+  method logic_ctor_info fmt ci =  fprintf fmt "%a" self#logic_name ci.ctor_name
 
   method initinfo fmt io =
     match io.init with
@@ -2401,7 +2401,7 @@ class cil_printer () = object (self)
         if Kernel.Unicode.get () then Utf8_logic.real else "real"
       in
       Format.fprintf fmt "%s%t" res pname
-    | Ltype ({ lt_name = name},[]) when name = Utf8_logic.boolean->
+    | Ltype ({ lt_name = name},[]) when name = Utf8_logic.boolean ->
       let res =
         if Kernel.Unicode.get () then Utf8_logic.boolean else "boolean"
       in
@@ -2417,7 +2417,7 @@ class cil_printer () = object (self)
       fprintf fmt "@[@[<2>{@ %a@]}@]%a%t"
         (Pretty_utils.pp_list ~sep:",@ " (self#logic_type None)) args
         (self#logic_type None) rt pname
-    | Lvar s -> fprintf fmt "%a%t" self#varname s pname
+    | Lvar s -> fprintf fmt "%s%t" s pname
 
   method private name fmt s =
     if needs_quote s then Format.fprintf fmt "\"%s\"" s
@@ -2539,7 +2539,7 @@ class cil_printer () = object (self)
            (Pretty_utils.pp_list
               ~sep:",@ " ~pre:"@[<hov>" ~suf:"@]@;" self#term_node) l
        | _ ->
-         fprintf fmt "%a%a" self#varname ci.ctor_name
+         fprintf fmt "%a%a" self#logic_name ci.ctor_name
            (Pretty_utils.pp_list ~pre:"(@[" ~suf:"@])" ~sep:",@ " self#term)
            args)
     | TLval lv -> fprintf fmt "%a" (self#term_lval_prec current_level) lv
@@ -2721,6 +2721,18 @@ class cil_printer () = object (self)
   method term_lhost fmt (lh:term_lhost) =
     self#term_lval fmt (lh, TNoOffset)
 
+
+  val module_stack : string Stack.t = Stack.create ()
+
+  method logic_name fmt a =
+    try
+      let prefix = Stack.top module_stack in
+      match Extlib.string_del_prefix prefix a with
+      | Some x -> pp_print_string fmt x
+      | None -> self#varname fmt a
+    with Stack.Empty ->
+      self#varname fmt a
+
   method logic_info fmt li = self#logic_var fmt li.l_var_info
 
   method logic_var fmt v =
@@ -2731,7 +2743,7 @@ class cil_printer () = object (self)
        | Some v -> Format.fprintf fmt "vid:%d, " v.vid);
       Format.fprintf fmt "lvid:%d */" v.lv_id
     end;
-    self#varname fmt v.lv_name
+    self#logic_name fmt v.lv_name
 
   method quantifiers fmt l =
     Pretty_utils.pp_list ~sep:",@ "
@@ -3308,7 +3320,7 @@ class cil_printer () = object (self)
       let old_lab = current_label in
       fprintf fmt "@[<hv 2>@[<hov 1>%a %a%a%a:@]@ %t%a;@]@\n"
         self#pp_lemma_kind pred.tp_kind
-        self#varname name
+        self#logic_name name
         self#labels labels
         self#polyTypePrms tvars
         (* pretty printing of lemma statement is done inside an environment
@@ -3322,7 +3334,7 @@ class cil_printer () = object (self)
     | Dtype (ti,_) ->
       fprintf fmt "@[<hv 2>@[%a %a%a%a;@]@\n"
         self#pp_acsl_keyword "type"
-        self#varname ti.lt_name self#polyTypePrms ti.lt_params
+        self#logic_name ti.lt_name self#polyTypePrms ti.lt_params
         (fun fmt -> function
            | None -> fprintf fmt "@]"
            | Some d -> fprintf fmt " =@]@ %a" self#logic_type_def d)
@@ -3412,12 +3424,21 @@ class cil_printer () = object (self)
            self#global_annotation)
         decls
     | Dmodule(id,decls,_attr, _) ->
-      (* attributes are meant to be purely internal for now. *)
-      fprintf fmt "@[<v 2>@[%a %s {@]@\n%a}@]@\n"
-        self#pp_acsl_keyword "module" id
-        (Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
-           self#global_annotation)
-        decls
+      begin
+        (* attributes are meant to be purely internal for now. *)
+        fprintf fmt "@[<v 2>@[%a %a {@]"
+          self#pp_acsl_keyword "module" self#logic_name id ;
+        try
+          Stack.push (id ^ "::") module_stack ;
+          fprintf fmt "@\n%a}@]@\n"
+            (Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
+               self#global_annotation)
+            decls ;
+          ignore @@ Stack.pop module_stack ;
+        with err ->
+          ignore @@ Stack.pop module_stack ;
+          raise err
+      end
     | Dextended (e,_attr,_) -> self#extended fmt e
 
   method logic_type_def fmt = function

src/kernel_services/ast_printing/logic_print.ml

@@ -39,6 +39,9 @@ let print_constant fmt = function
 
 let module_prefix : string Stack.t = Stack.create ()
 
+let module_name a =
+  try Stack.top module_prefix ^ a with Stack.Empty -> a
+
 let print_qid fmt name =
   try
     let prefix = Stack.top module_prefix in
@@ -390,7 +393,7 @@ let rec print_decl fmt d =
   | LDmodule (name,ds) ->
     begin
       try
-        Stack.push (name ^ "::") module_prefix ;
+        Stack.push (module_name name ^ "::") module_prefix ;
         fprintf fmt "@[<2>module@ %s@ {@\n%a@]@\n}" name
           (pp_list ~sep:"@\n" print_decl) ds ;
         ignore @@ Stack.pop module_prefix ;

src/kernel_services/ast_printing/printer_api.ml

@@ -274,6 +274,7 @@ class type extensible_printer_type = object
   method builtin_logic_info: Format.formatter -> builtin_logic_info -> unit
   method logic_type_info: Format.formatter -> logic_type_info -> unit
   method logic_ctor_info: Format.formatter -> logic_ctor_info -> unit
+  method logic_name: Format.formatter -> string -> unit
   method logic_var: Format.formatter -> logic_var -> unit
   method quantifiers: Format.formatter -> quantifiers -> unit
   method predicate_node: Format.formatter -> predicate_node -> unit

tests/spec/module.i

@@ -11,7 +11,7 @@
   }
   module foo::Jazz {
     import foo::Bar \as X;
-    logic t inv(t x);
+    logic t inv(X::t x);
     logic t opN(t x, integer n) = n >= 0 ? X::opN(x,n) : X::opN(inv(x),-n);
   }
   import foo::Bar \as A;

tests/spec/oracle/module.res.oracle

@@ -2,23 +2,22 @@
 /* Generated by Frama-C */
 /*@
 module foo::Bar {
-  type foo::Bar::t;
+  type t;
   
-  logic foo::Bar::t foo::Bar::e;
+  logic t e;
   
-  logic foo::Bar::t foo::Bar::op(foo::Bar::t x, foo::Bar::t y) ;
+  logic t op(t x, t y) ;
   
-  logic foo::Bar::t foo::Bar::opN(foo::Bar::t x, ℤ n) =
-    n ≥ 0? foo::Bar::op(x, foo::Bar::opN(x, n - 1)): foo::Bar::e;
+  logic t opN(t x, ℤ n) = n ≥ 0? op(x, opN(x, n - 1)): e;
   
   }
  */
 /*@
 module foo::Jazz {
-  logic foo::Bar::t foo::Jazz::inv(foo::Bar::t x) ;
+  logic foo::Bar::t inv(foo::Bar::t x) ;
   
-  logic foo::Bar::t foo::Jazz::opN(foo::Bar::t x, ℤ n) =
-    n ≥ 0? foo::Bar::opN(x, n): foo::Bar::opN(foo::Jazz::inv(x), -n);
+  logic foo::Bar::t opN(foo::Bar::t x, ℤ n) =
+    n ≥ 0? foo::Bar::opN(x, n): foo::Bar::opN(inv(x), -n);
   
   }
  */