From 56552fc3c6e4e275a3f1a2cf77400a37850ef58f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Nov 2021 16:57:34 +0100
Subject: [PATCH] [obfuscate] Obfuscates axiomatics and lemmas

Since we modify the AST anyways, there's no reason to leave these names unchanged.
---
 src/plugins/obfuscator/obfuscate.ml        | 13 +++++++------
 src/plugins/obfuscator/obfuscator_kind.ml  |  6 ++++++
 src/plugins/obfuscator/obfuscator_kind.mli |  2 ++
 tests/misc/oracle/obfuscate.res.oracle     | 14 ++++++++------
 4 files changed, 23 insertions(+), 12 deletions(-)

diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index 3decde3ce5c..ce98d742858 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -166,12 +166,13 @@ class visitor = object
     Cil.DoChildren
 
   method! vannotation = function
-    | Daxiomatic(str, _, _, _) ->
-      warn "axiomatic" str;
-      Cil.DoChildren
-    | Dlemma(str, _, _, { tp_kind }, _, _) ->
-      warn (Cil_printer.string_of_lemma tp_kind) str;
-      Cil.DoChildren
+    | Daxiomatic(str, globs, attrs, loc) ->
+      let str' = Dictionary.fresh Obfuscator_kind.Axiomatic str in
+      Cil.ChangeDoChildrenPost(Daxiomatic(str',globs,attrs,loc),Extlib.id)
+    | Dlemma(str, labs, typs, pred, attrs, loc) ->
+      let str' = Dictionary.fresh Obfuscator_kind.Lemma str in
+      Cil.ChangeDoChildrenPost(
+        Dlemma(str',labs,typs, pred, attrs, loc),Extlib.id)
     | _ ->
       Cil.DoChildren
 
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index e1f1513784a..1e5c410045b 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -36,6 +36,8 @@ type k =
   | Type
   | Logic_type
   | Logic_constructor
+  | Axiomatic
+  | Lemma
 
 let name_of_kind = function
   | Behavior -> "behavior"
@@ -53,6 +55,8 @@ let name_of_kind = function
   | Type -> "type"
   | Logic_type -> "logic type"
   | Logic_constructor -> "logic constructor"
+  | Axiomatic -> "axiomatic"
+  | Lemma -> "lemma"
 
 let prefix = function
   | Behavior -> "B"
@@ -70,6 +74,8 @@ let prefix = function
   | Type -> "T"
   | Logic_type -> "LT"
   | Logic_constructor -> "LC"
+  | Axiomatic -> "A"
+  | Lemma -> "LE"
 
 include Datatype.Make_with_collections
     (struct
diff --git a/src/plugins/obfuscator/obfuscator_kind.mli b/src/plugins/obfuscator/obfuscator_kind.mli
index 75fd6bb8af5..8eee3ce7ad4 100644
--- a/src/plugins/obfuscator/obfuscator_kind.mli
+++ b/src/plugins/obfuscator/obfuscator_kind.mli
@@ -36,6 +36,8 @@ type k =
   | Type
   | Logic_type
   | Logic_constructor
+  | Axiomatic
+  | Lemma
 
 include Datatype.S_with_collections with type t = k
 val prefix: t -> string
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index e36f5683039..2f53420c9b5 100644
--- a/tests/misc/oracle/obfuscate.res.oracle
+++ b/tests/misc/oracle/obfuscate.res.oracle
@@ -2,12 +2,12 @@
 [obfuscator] Warning: unobfuscated attribute name `fc_stdlib'
 [obfuscator] Warning: unobfuscated attribute parameter name `stdint.h'
 [obfuscator] Warning: unobfuscated attribute name `missingproto'
-[obfuscator] Warning: unobfuscated axiomatic name `A'
-[obfuscator] Warning: unobfuscated axiomatic name `A1'
-[obfuscator] Warning: unobfuscated lemma name `OK'
 /* *********************************** */
 /* start of dictionary for obfuscation */
 /* *********************************** */
+// axiomatics
+#define A1 A
+#define A2 A1
 // behaviors
 #define B1 bhv
 // enums
@@ -31,6 +31,8 @@
 // logic constructors
 #define LC1 T
 #define LC2 F
+// lemmas
+#define LE1 OK
 // logic types
 #define LT1 t
 // logic variables
@@ -172,12 +174,12 @@ void F6(struct T2 *f6)
   return;
 }
 
-/*@ axiomatic A {
+/*@ axiomatic A1 {
       predicate LV3(void (*LV4)()) ;
       
       }
  */
-/*@ axiomatic A1 {
+/*@ axiomatic A2 {
       predicate LV5(void (*LV6)()) ;
       
       }
@@ -188,7 +190,7 @@ void F7(void)
   return;
 }
 
-/*@ lemma OK{L}: LV3((void (*)())(&F7)) ∧ LV5((void (*)())(&F7));
+/*@ lemma LE1{L}: LV3((void (*)())(&F7)) ∧ LV5((void (*)())(&F7));
 
 */
 
-- 
GitLab