From 18b5e1acc6671230f5e77baeb621e914f1bbd197 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Fri, 29 Apr 2022 18:22:41 +0200
Subject: [PATCH] Bug resolved on guard handling in ProVerif generation
---
.../avatartranslator/AvatarBinaryGuard.java | 4 ++++
.../avatartranslator/AvatarComposedGuard.java | 5 +++-
.../AvatarSimpleGuardDuo.java | 24 +++++++++++++++++++
.../toproverif/AVATAR2ProVerif.java | 23 +++++++++++-------
4 files changed, 46 insertions(+), 10 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarBinaryGuard.java b/src/main/java/avatartranslator/AvatarBinaryGuard.java
index 070ef547e6..13771149cf 100644
--- a/src/main/java/avatartranslator/AvatarBinaryGuard.java
+++ b/src/main/java/avatartranslator/AvatarBinaryGuard.java
@@ -38,6 +38,8 @@
package avatartranslator;
+import myutil.TraceManager;
+
import java.util.Map;
/**
@@ -74,6 +76,8 @@ public class AvatarBinaryGuard extends AvatarComposedGuard {
return this.guardA.getAsString (translator) + translator.translateBinaryOp (this.binaryOp) + this.guardB.getAsString (translator);
}
+
+
@Override
public AvatarBinaryGuard clone () {
return new AvatarBinaryGuard (this.guardA.clone (), this.guardB.clone (), this.binaryOp);
diff --git a/src/main/java/avatartranslator/AvatarComposedGuard.java b/src/main/java/avatartranslator/AvatarComposedGuard.java
index af75da1a4e..b4e1a3c08f 100644
--- a/src/main/java/avatartranslator/AvatarComposedGuard.java
+++ b/src/main/java/avatartranslator/AvatarComposedGuard.java
@@ -38,6 +38,8 @@
package avatartranslator;
+import myutil.TraceManager;
+
/**
* Class AvatarComposedGuard
* Creation: 16/09/2015
@@ -47,7 +49,8 @@ package avatartranslator;
public abstract class AvatarComposedGuard extends AvatarGuard {
public AvatarComposedGuard getOpposite () {
- //return new AvatarUnaryGuard ("not", "(", ")", this);
+
+ // Otherwise, general case:
return new AvatarUnaryGuard ("", "(", ") == false", this);
}
diff --git a/src/main/java/avatartranslator/AvatarSimpleGuardDuo.java b/src/main/java/avatartranslator/AvatarSimpleGuardDuo.java
index d6aa10cb0a..e5ff575d7b 100644
--- a/src/main/java/avatartranslator/AvatarSimpleGuardDuo.java
+++ b/src/main/java/avatartranslator/AvatarSimpleGuardDuo.java
@@ -98,4 +98,28 @@ public class AvatarSimpleGuardDuo extends AvatarSimpleGuard {
this.termB.replaceAttributes (attributesMapping);
}
}
+
+ public AvatarComposedGuard getOpposite () {
+ //return new AvatarUnaryGuard ("not", "(", ")", this);
+
+ // If guard is a binary guard, we take its opposite
+
+ String op = "";
+ if (binaryOp == "==") {
+ op = "!=";
+ } else if (binaryOp == "!=") {
+ op = "==";
+ }
+
+ if (op == null) {
+ // Otherwise, general case:
+ return new AvatarUnaryGuard("", "(", ") == false", this);
+ }
+
+ AvatarSimpleGuardDuo g = this.clone();
+ g.binaryOp = op;
+
+ return g;
+
+ }
}
diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
index b5f23c4898..c9fc22f0e4 100755
--- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -352,16 +352,18 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// -> transformed into a = b, a <> b, g1 && g2, g1 || g2
// Returns nulls otherwise
private static String translateGuard (AvatarGuard _guard, Map<AvatarAttribute, Integer> attributeCmp) {
- TraceManager.addDev(_guard.toString());
- if (_guard == null || _guard instanceof AvatarGuardEmpty)
+ TraceManager.addDev("Handling Guard:" + _guard.toString());
+ if (_guard == null || _guard instanceof AvatarGuardEmpty) {
+ TraceManager.addDev("Null or empty guard");
return null;
+ }
if (_guard instanceof AvatarGuardElse)
// TODO: warning
return null;
if (_guard instanceof AvatarSimpleGuardMono) {
- //TraceManager.addDev("SimpleGuardMono:" + _guard);
+ TraceManager.addDev("SimpleGuardMono:" + _guard);
String term = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardMono) _guard).getTerm (), attributeCmp);
//TraceManager.addDev("guard/ term=" + term);
if (term != null)
@@ -371,7 +373,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarSimpleGuardDuo) {
- //TraceManager.addDev("SimpleGuardDuo");
+ TraceManager.addDev("SimpleGuardDuo");
String delim = null;
String termA = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermA (), attributeCmp);
String termB = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermB (), attributeCmp);
@@ -392,7 +394,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarUnaryGuard) {
- //TraceManager.addDev("UnaryGuard");
+ TraceManager.addDev("UnaryGuard");
String unary = ((AvatarUnaryGuard) _guard).getUnaryOp ();
AvatarGuard guard = ((AvatarUnaryGuard) _guard).getGuard ();
@@ -406,6 +408,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
String guardProV = AVATAR2ProVerif.translateGuard (guard, attributeCmp);
+
+
if (beforeProV != null && guardProV != null)
return beforeProV + guardProV + afterProV;
@@ -413,7 +417,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarBinaryGuard) {
- //TraceManager.addDev("BinaryGuard");
+ TraceManager.addDev("BinaryGuard");
String delim = ((AvatarBinaryGuard) _guard).getBinaryOp ();
AvatarGuard guardA = ((AvatarBinaryGuard) _guard).getGuardA ();
AvatarGuard guardB = ((AvatarBinaryGuard) _guard).getGuardB ();
@@ -433,7 +437,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarConstantGuard) {
- //TraceManager.addDev("ConstantGuard");
+ TraceManager.addDev("ConstantGuard");
AvatarConstantGuard constant = (AvatarConstantGuard) _guard;
if (constant.getConstant () == AvatarConstant.TRUE)
return "TRUE";
@@ -441,6 +445,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
return "FALSE";
}
+ TraceManager.addDev("No valid guard found");
return null;
}
@@ -1367,8 +1372,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
AvatarAttributeState attrB = ((AvatarPragmaAuthenticity) pragma).getAttrB ();
if (attrA.getAttribute ().getBlock () == arg.block && attrA.getState ().getName ().equals (_asme.getName ())) {
TraceManager.addDev ("DEBUG: " + attrA.getAttribute ());
- TraceManager.addDev ("DEBUG: " + attrA.getAttribute ().getBlock ());
- TraceManager.addDev ("DEBUG: " + arg.attributeCmp.get (attrA.getAttribute()));
+ //TraceManager.addDev ("DEBUG: " + attrA.getAttribute ().getBlock ());
+ //TraceManager.addDev ("DEBUG: " + arg.attributeCmp.get (attrA.getAttribute()));
String sp = "authenticity" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), _asme.getName ()) + " (" + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), arg.attributeCmp.get (attrA.getAttribute ()).toString ()) + ")";
if (!authenticityEvents.contains (sp)) {
authenticityEvents.add (sp);
--
GitLab