Merge branch 'fix/obfuscator/issue490' into 'master'

Fix/obfuscator/issue490

Closes #490

See merge request frama-c/frama-c!2175

Changelog

@@ -17,6 +17,7 @@
 Open Source Release <next-release>
 ##################################
 
+-*  Obfuscator [2019/02/26] Obfuscate logic types and logic constructors.
 -   Eva       [2019/01/10] Improved precision on nested loops (by postponing
               the widening on inner loops according to -eva-widening-period).
 -   Kernel    [2019/01/03] Add attributes for loop statements to allow

src/kernel_services/ast_data/cil_types.mli

@@ -1487,7 +1487,7 @@ and logic_body =
 (** Description of a logic type.
     @plugin development guide *)
 and logic_type_info = {
-  lt_name: string;
+  mutable lt_name: string;
   lt_params : string list; (** type parameters*)
   mutable lt_def: logic_type_def option;
     (** definition of the type. None for abstract types. *)
@@ -1528,7 +1528,7 @@ and logic_var = {
 (** Description of a constructor of a logic sum-type.
     @plugin development guide *)
 and logic_ctor_info =
- { ctor_name: string; (** name of the constructor. *)
+ { mutable ctor_name: string; (** name of the constructor. *)
    ctor_type: logic_type_info; (** type to which the constructor belongs. *)
    ctor_params: logic_type list 
  (** types of the parameters of the constructor. *)

src/plugins/obfuscator/obfuscate.ml

@@ -38,7 +38,8 @@ class visitor = object
 
   method! vglob_aux = function
   | GType (ty,_) ->
-    ty.tname <- Dictionary.fresh Obfuscator_kind.Type ty.tname; 
+    if not (Cil.typeHasAttribute "fc_stdlib" ty.ttype) then
+      ty.tname <- Dictionary.fresh Obfuscator_kind.Type ty.tname;
     Cil.DoChildren
   | GVarDecl (v, _) | GVar (v, _, _) | GFun ({svar = v}, _) | GFunDecl (_, v, _)
       when Cil.is_unused_builtin v ->
@@ -83,10 +84,15 @@ class visitor = object
     if Varinfo.Hashtbl.mem varinfos_visited vi then
       Cil.SkipChildren
     else begin
-      if Cil.isFunctionType vi.vtype then begin
-	if vi.vname <> "main" then 
-	  vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname
-      end else begin
+      if Cil.isFunctionType vi.vtype then
+        try
+          if vi.vname <> "main"
+          && not (Cil.is_builtin vi)
+          && not (Cil.is_special_builtin vi.vname)
+          && not (Cil.hasAttribute "fc_stdlib" vi.vattr) then
+            vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname
+        with Not_found -> assert false
+      else begin
 	let add =
           if vi.vglob then Dictionary.fresh Obfuscator_kind.Global_var
           else if vi.vformal then Dictionary.fresh Obfuscator_kind.Formal_var
@@ -157,11 +163,15 @@ class visitor = object
     Cil.DoChildren
 
   method! vlogic_type_info_decl lti =
-    warn "logic type" lti.lt_name;
+    if not (Logic_env.is_builtin_logic_type lti.lt_name)
+    then lti.lt_name <- Dictionary.fresh Obfuscator_kind.Logic_type lti.lt_name ;
     Cil.DoChildren
 
   method! vlogic_ctor_info_decl lci =
-    warn "logic constructor" lci.ctor_name;
+    if not (Logic_env.is_builtin_logic_ctor lci.ctor_name)
+    then
+      lci.ctor_name <-
+        Dictionary.fresh Obfuscator_kind.Logic_constructor lci.ctor_name ;
     Cil.DoChildren
 
   method! vattr = function

src/plugins/obfuscator/obfuscator_kind.ml

@@ -33,7 +33,9 @@ type k =
   | Logic_var
   | Predicate
   | Type
-      
+  | Logic_type
+  | Logic_constructor
+
 let name_of_kind = function
   | Behavior -> "behavior"
   | Enum -> "enum"
@@ -47,6 +49,8 @@ let name_of_kind = function
   | Logic_var -> "logic variable"
   | Predicate -> "predicate"
   | Type -> "type"
+  | Logic_type -> "logic type"
+  | Logic_constructor -> "logic constructor"
 
 let prefix = function
   | Behavior -> "B"
@@ -61,6 +65,8 @@ let prefix = function
   | Logic_var -> "LV"
   | Predicate -> "P"
   | Type -> "T"
+  | Logic_type -> "LT"
+  | Logic_constructor -> "LC"
 
 include Datatype.Make_with_collections
 (struct

src/plugins/obfuscator/obfuscator_kind.mli

@@ -33,6 +33,8 @@ type k =
   | Logic_var
   | Predicate
   | Type
+  | Logic_type
+  | Logic_constructor
 
 include Datatype.S_with_collections with type t = k
 val prefix: t -> string

tests/misc/obfuscate.i → tests/misc/obfuscate.c

@@ -46,3 +46,16 @@ int logic(int f1)
 int main(int* p) { 
   if ("ti\rti" == "ti\rti") f(p); 
 }
+
+/* Obfuscate logic types and logic constructors. */
+/*@ type t = T | F; */
+
+#include "stdint.h"
+
+/* Do not obfuscate builtins and stdlib types and functions. */
+int builtin_and_stdlib () {
+  int32_t x = 42;
+  Frama_C_show_each(x);
+  /*@ assert \true; */
+  return 1;
+}

tests/misc/oracle/obfuscate.res.oracle

-[kernel] Parsing tests/misc/obfuscate.i (no preprocessing)
+[kernel] Parsing tests/misc/obfuscate.c (with preprocessing)
+[obfuscator] Warning: unobfuscated attribute name `fc_stdlib'
+[obfuscator] Warning: unobfuscated attribute parameter name `stdint.h'
+[obfuscator] Warning: unobfuscated attribute name `missingproto'
 /* *********************************** */
 /* start of dictionary for obfuscation */
 /* *********************************** */
@@ -12,11 +15,17 @@
 #define F1 my_func
 #define F2 f
 #define F3 logic
+#define F4 builtin_and_stdlib
 // global variables
 #define G1 my_var
 // labels
 #define L1 end
 #define L2 end
+// logic constructors
+#define LC1 T
+#define LC2 F
+// logic types
+#define LT1 t
 // logic variables
 #define LV1 I
 #define LV2 x
@@ -29,6 +38,8 @@
 #define V2 __retres
 #define V3 V1
 #define V4 __retres
+#define V5 x
+#define V6 __retres
 // formal variables
 #define f1 p
 #define f2 f1
@@ -47,6 +58,7 @@
 /* ********************************************************* */
 
 /* Generated by Frama-C */
+#include "stdint.h"
 enum T1 {
     E1 = 0,
     E2 = 1,
@@ -54,7 +66,8 @@ enum T1 {
 };
 int G1 = 0;
 /*@ global invariant LV1: G1 ≥ 0;
- */
+
+*/
 /*@ requires G1 > 0;
     ensures G1 > \old(G1);
     ensures ∀ ℤ LV2; LV2 ≡ LV2;
@@ -102,4 +115,19 @@ int main(int *f3)
   return V4;
 }
 
+/*@ type LT1 = LC1 | LC2;
+
+*/
+extern int ( /* missing proto */ Frama_C_show_each)();
+
+int F4(void)
+{
+  int V6;
+  int32_t V5 = 42;
+  Frama_C_show_each(V5);
+  /*@ assert \true; */ ;
+  V6 = 1;
+  return V6;
+}
+