diff --git a/.idea/.name b/.idea/.name new file mode 100644 index 0000000..a501d11 --- /dev/null +++ b/.idea/.name @@ -0,0 +1 @@ +LiSATutorial \ No newline at end of file diff --git a/.idea/codeStyles/Project.xml b/.idea/codeStyles/Project.xml new file mode 100644 index 0000000..919ce1f --- /dev/null +++ b/.idea/codeStyles/Project.xml @@ -0,0 +1,7 @@ + + + + + + \ No newline at end of file diff --git a/.idea/codeStyles/codeStyleConfig.xml b/.idea/codeStyles/codeStyleConfig.xml index 3e682c6..a55e7a1 100644 --- a/.idea/codeStyles/codeStyleConfig.xml +++ b/.idea/codeStyles/codeStyleConfig.xml @@ -1,5 +1,5 @@ - \ No newline at end of file diff --git a/.idea/misc.xml b/.idea/misc.xml index 573ac85..31c600a 100644 --- a/.idea/misc.xml +++ b/.idea/misc.xml @@ -1,7 +1,10 @@ - + + + + \ No newline at end of file diff --git a/.idea/shelf/Uncommitted_changes_before_Update_at_06_04_2025,_13_22_[Changes]/shelved.patch b/.idea/shelf/Uncommitted_changes_before_Update_at_06_04_2025,_13_22_[Changes]/shelved.patch new file mode 100644 index 0000000..eb460d9 --- /dev/null +++ b/.idea/shelf/Uncommitted_changes_before_Update_at_06_04_2025,_13_22_[Changes]/shelved.patch @@ -0,0 +1,20 @@ +Index: .idea/misc.xml +IDEA additional info: +Subsystem: com.intellij.openapi.diff.impl.patch.BaseRevisionTextPatchEP +<+>\n\n \n \n \n \n +Subsystem: com.intellij.openapi.diff.impl.patch.CharsetEP +<+>UTF-8 +=================================================================== +diff --git a/.idea/misc.xml b/.idea/misc.xml +--- a/.idea/misc.xml (revision 7aac3ade45ecc9c82a70a7d2bb9ed7fa602caece) ++++ b/.idea/misc.xml (date 1743938523888) +@@ -1,7 +1,7 @@ + + + +- ++ + + + +\ No newline at end of file diff --git a/.idea/shelf/Uncommitted_changes_before_Update_at_06_04_2025__13_22__Changes_.xml b/.idea/shelf/Uncommitted_changes_before_Update_at_06_04_2025__13_22__Changes_.xml new file mode 100644 index 0000000..3af7e3e --- /dev/null +++ b/.idea/shelf/Uncommitted_changes_before_Update_at_06_04_2025__13_22__Changes_.xml @@ -0,0 +1,4 @@ + + \ No newline at end of file diff --git a/README.md b/README.md index 1a6bc07..0155252 100644 --- a/README.md +++ b/README.md @@ -1,13 +1,452 @@ -# LiSA tutorials +# Rapport : Analyse Statique avec LISA +- `IntervalSafeOverflowDomain`: Domaine non relationnel abstrait des intervalles prenant en compte les dépassements (difficulté : 4) +- `TwoVariablesInequalityDomain`: Domaine relationnel abstrait de deux variables par inéquation linéaire (difficulté : 4) +- `IntervalSafeOverflowTwoVariablesInequalityCartesianProduct` : Produit cartésien de ces 2 domaines abstraits -This repository contains the code developed and used during LiSA's tutorials. Every tutorial is listed together with a link to the slides used and the tag of the code shown during the tutorial itself. +# **Domaine non rélationnel** -## Tutorials given +Cette prémière partie explique l'analyse des exemples de code fournis en relation avec les concepts d'opérations arithmétiques, de structures conditionnelles, de boucles, et leur gestion à l'aide du domaine abstrait `IntervalSafeOverflowDomain`. Ce domaine est conçu pour assurer une évaluation sécurisée et correcte des valeurs numériques dans un programme tout en évitant les dépassements d'entiers (overflows). -- PLDI '24 [[slides]](https://docs.google.com/presentation/d/1-oFl5Lgg-6mu0IdXMv8u-9w_ypc1aYbg-t_t8HVQBjw/edit?usp=sharing) [[code used]](https://github.com/lisa-analyzer/lisa-tutorial/releases/tag/pldi24) +--- -- Lipari Summer School '24 [[slides]](https://docs.google.com/presentation/d/16MYOHTZJuuzuym9tcIH4L2r24Kn11vjAq7vpyTGcv14/edit?usp=sharing) [[code used]](https://github.com/lisa-analyzer/lisa-tutorial/releases/tag/lipari24) +### Classe Principale : `IntervalSafeOverflowDomain.java` +### Classe Test : `IntervalleSafeOverflowTest.java` +### Input : `ìntervalleSafeOverflow.imp` -- Ca' Foscari PhD Course - [[code used]](https://github.com/lisa-analyzer/lisa-tutorial/releases/tag/ssv24) +--- +## 1. Opérations arithmétiques dans `basic()` +### Code étudié : +``` +basic() { + def i = 2147483647; + def j = 20; + def k = -j; + def a = i + j; + def s = i - j; + def m = i * j; + def d = i / j; +} +``` +### Analyse et explication : +Ce code inclut des opérations arithmétiques de base : +- **Addition (`i + j`)** : Calcule la somme de deux valeurs. +- **Soustraction (`i - j`)** : Soustrait une valeur de l'autre. +- **Multiplication (`i * j`)** : Calcule le produit de deux valeurs. +- **Division entière (`i / j`)** : Divise les deux nombres en arrondissant le résultat vers zéro. +- **Négation (`-j`)** : Inverse le signe de la valeur. -- Seminar at University of Verona - [[code used]](https://github.com/lisa-analyzer/lisa-tutorial/releases/tag/univr25) +### Gestion par `IntervalSafeOverflowDomain` : +Le domaine abstrait `IntervalSafeOverflowDomain` est capable d'effectuer ces calculs de manière sûre grâce à : +- Une représentation des intervalles numériques comme `[low..high]`. +- Une prise en charge explicite des dépassements d'entiers : + - Si une addition, soustraction ou multiplication dépasse les limites de l'intervalle entier (`[-2^31, 2^31-1]`), l'intervalle est ajusté sans provoquer d'erreurs. + +- Les fonctions comme `add`, `sub`, `mul` et `div` encapsulent ces comportements et gèrent les valeurs infinies et les cas limites (comme la division par zéro). +- Les + +# Résultat des analyses et des intervalles + +Voici les intervalles correspondant aux variables utilisées, calculés après l'analyse abstraite effectuée via le domaine `IntervalSafeOverflowDomain` : + +- **a** : `[-2147483629 .. -2147483629]` + Indique que la valeur de `a` est connue avec certitude et est exactement égale à `-2147483629`. Ceci est l'impacte directe de la façon dont nous avons géré l'overflow. Un dépassement de la borne supérieure positive nous renvoie dans la borne inférieure négative. + +- **d** : `[107374182 .. 107374182]` + Résultat de la division. La valeur est fixe et se situe exactement dans cet intervalle. + +- **i** : `[+∞ .. +∞]` + La variable `i` est considérée comme ayant une valeur infinie positive. + +- **j** : `[20 .. 20]` + La valeur de `j` est connue et fixe, égale à `20`. + +- **k** : `[-20 .. -20]` + Résultat de la négation de `j`. La valeur est fixe et égale à `-20`. + +- **m** : `[-20 .. -20]` + Multiplier deux valeurs aboutit ici à cet intervalle constant. + +- **s** : `[2147483627 .. 2147483627]` + Résultat d'une soustraction, où la valeur est fixe et égale au nombre spécifié. + +Ces intervalles montrent la précision de l'analyse abstraite, qui détermine les bornes exactes ou approximatives des valeurs des variables à chaque point du programme. + +## 2. **Structure conditionnelle `if` dans `ifstatement()`** +### Code étudié : +``` +ifstatement() { + def i = 0; + if(i > 0) + i = 1; + else + def j = i * 2; +} +``` + +### Analyse et explication : +Ce code illustre une structure conditionnelle où la variable `i` est testée dans une condition : +- Si `i > 0`, sa valeur est modifiée (`i = 1`). +- Sinon, une nouvelle variable `j` est introduite en utilisant l'expression `i * 2`. + +### Gestion par `IntervalSafeOverflowDomain` : +Le domaine abstrait gère ce type de logique via des **raffinements d'intervalles** : +- Lorsqu’une condition comme `i > 0` est rencontrée, le domaine ajuste dynamiquement les bornes de l'intervalle de `i` : + - Dans la branche "true", l'intervalle devient `[1..+∞]`. + - Dans la branche "false", l'intervalle devient `[-∞..0]`. + +- Ces raffinements permettent de réduire les cas possibles pour les variables et d’optimiser l’analyse dans les deux branches. Il est géré dans la méthode `assumeBinary` et fait appel la méthode `lubAux` pour l'opérateur *LeastUpperBound*. + +## 3. **Boucle `while` dans `whilestatement()`** +### Code étudié : +``` +whilestatement() { + def a = -2; + def x = 0; + while(a >= 1) + x = x + 2; +} +``` +### Analyse et explication : +Le bloc de code utilise une boucle `while` avec la condition `a >= 1`. Cependant, dans ce cas précis : +- La variable `a` est initialisée à `-2`, et la condition est immédiatement fausse. +- La boucle ne s'exécute jamais (`dead code`). + +### Code étudié (widening) : +``` +wideningwhilestatement() { + def a = 0; + def x = 1; + while(a<=10) { + x = x * 2; + a = a + 1; + } + } +``` +- À la différence de l'autre instruction de boucle `while`, + celle-ci a eu recours à la méthode `widening`, à partir du 5-ème pour atteindre rapidement un point fixe et garantir la terminaison de la boucle. +- **a** : `[-∞ .. 11]` +- **x** : `[2 .. +∞]` + + +### Gestion par `IntervalSafeOverflowDomain` : +Le domaine abstrait gère les boucles en utilisant une **approximation via élargissement (`widening`)** : +- Si la condition incluait une mise à jour de la valeur de `a` (par exemple, `a -= 1`), le domaine utiliserait l'élargissement pour calculer une approximation sûre et terminer l'analyse. +- Cependant, comme la condition est statiquement fausse (`a = -2 < 1`), l'analyse conclut rapidement que la boucle est non atteignable, ce qui optimise le processus global. + +## 4. **Fonctionnement de `IntervalSafeOverflowDomain`** +La classe `IntervalSafeOverflowDomain` implémente un domaine abstrait basé sur les **intervalles** `[low..high]` pour les variables. Voici ses fonctionnalités principales : +### Représentation : +- Chaque variable est associée à un intervalle, représentant toutes les valeurs possibles qu’elle peut prendre au moment de l’analyse. +- Le domaine prend en charge des bornes infinies positives (`+∞`) ou négatives (`-∞`) pour modéliser des intervalles non bornés. + +### Opérations supportées : +1. **Addition, soustraction, multiplication et division** entre intervalles. +2. Gestion des **infinis** et des situations limites (par exemple, division par zéro). +3. Négation numérique, raffinements de bornes et gestion des dépassements d'entiers (overflow). + +### Raffinement conditionnel : +Lors de tests basés sur des comparaisons (comme `x < 5` ou `y >= 0`), le domaine refactorise dynamiquement l'intervalle des variables en fonction de la condition testée. +### Boucles (`while`) : +Les boucles sont analysées à l'aide de techniques d'élargissement pour garantir que l'analyse se termine toujours. +- Cela permet de calculer des bornes approximatives même lorsque le nombre d'itérations est inconnu. + +## 5. **Résumé** +Ce code prend en compte trois concepts fondamentaux dans l'analyse abstraite d'intervalles (domaine non rélationnel) : +1. **Opérations arithmétiques** : `IntervalSafeOverflowDomain` applique strictement des calculs sûrs pour éviter les dépassements (overflow) et gérer les bornes infinies. +2. **Structures conditionnelles (`if`)** : Le domaine raffine dynamiquement les intervalles dans chaque branche, optimisant la précision de l'analyse. +3. **Boucles (`while`)** : Grâce à l'élargissement, le domaine garantie une analyse toujours finie, même dans des boucles complexes. +4. **Possible amélioration** : Une amélioration de ce code consistera à traiter le `rand(a,b)`, `for`, `do ... while`. + +--- + +# **Domaine rélationnel** +La deuxième partie consiste à traite un domaine **TwoVariablesInequalityDomain** est un domaine abstrait relationnel dédié aux inéquations linéaires impliquant deux variables. Il est conçu pour analyser les relations linéaires (comme `ax + by ≤ c`) et simplifier ou étendre ces relations dans divers contextes programmatiques. Ce domaine peut être utilisé pour effectuer des analyses statiques sur des programmes afin de suivre des relations complexes entre variables avec précision. + +--- + +## Classe Principale : `TwoVariablesInequalityDomain.java` +## Classe Test : `TwoVariablesInequalityTest.java` +### Input : `TwoVariablesInequality.imp` + +--- +### Points Clés +1. **Constantes Domaines TOP et BOTTOM** : +- `TOP` : Domaine contenant toutes les relations possibles. +- `BOTTOM` : Domaine vide, représentant une contradiction. + +2. **Attributs** : +- `linearInequalities` : Représente l'ensemble des inéquations linéaires stockées sous forme simplifiée. +- Domaines Top et Bottom sont indiqués par des flags (`isTopDomain` et `isBottomDomain`). + +3. **Constructeurs** : +- Un constructeur simplifié permet d'initialiser avec des inéquations spécifiques tout en les réduisant et en supprimant les chevauchements inutiles. + +4. **Méthodes Principales** : +- **`assign`** : Gestion des affectations de variables permettant des mises à jour de relations. +- **`assume`** : Traitement des hypothèses exprimées sous forme d'inéquations à deux variables. +- **`lub`/`glb`** : Calcul du plus petit majorant (`lub`) et plus grand minorant (`glb`) entre deux domaines. +- **`processAndSimplifyLinearInequalities`** : Simplification des inéquations linéaires pour éviter la redondance et générer des relations dérivées par transitivité. + +--- + +## Représentation de l'Inéquation Linéaire : `LinearInequality` + +Chaque inéquation suit la forme générale : +**`a*x + b*y ≤ c`** + +### Attributs : +- **Coefficients des variables (`variableCoefficientsMap`)** : Une map associant chaque variable (de type `Identifier`) à son coefficient. +- **Constante droite (`c`)** : Valeur qui borne l'inéquation. +- **Type de contrainte** : + - Par défaut : `≤` + - Peut également être `<` (strict). + +### Simplification et Vérification : +1. **Détection de relations triviales** : +- Exemple : `0*x + 0*y ≤ c` où `c > 0` est considéré comme futile par `isTrivialInequality`. +2. **Vérification des inéquations mono-variables** : +- Les inéquations ne traitant qu'une seule variable sont généralement ignorées ou simplifiées via la méthode `isSingleVariableInequality`. +3. **Supprime les inéquations rédondantes** : +- Si l'environnement contient 2 ou plusieurs inéquations identiques, on ne retient qu'une seule. + 4.**Transitivité** : +- Les nouvelles relations sont générées en combinant les inéquations existantes (Ex. transitivité entre `x ≤ 5` et `x + y ≤ 7`). + Le **4** et **5** sont combiné dans l'implémentation de `processAndSimplifyLinearInequalities` + +--- + +## Fonctionnalités Clés + +### Manipulation de Variables : +1. **`assign`** : +- Permet de traiter les affectations dans le programme. +- Exemple : Si `u = z - 2`, alors une nouvelle inégalité `u - z <= -2` est ajoutée au domaine. + +2. **Mise à jour avec des Comparaisons** : +- Traite des expressions binaires de type `BinaryExpression` où l'opérateur est une comparaison (`ComparisonLe`). +- Simplifie des relations comme `(2*x + 5*y) <= 3`. + +### Gestion des Inéquations : +1. **Combinaisons et Réductions** : +- Génération d'un nouvel ensemble d'inéquations en fusionnant ou simplifiant par transitivité les existantes. +- Exemple : `x + y ≤ 5` combiné avec `x + y ≤ 3` pourrait produire `x + y ≤ 3`. + +2. **Support des Opérations Binaires** : +- Support pour `+`, `-`, et parfois pour `*` si l'un des termes est une constante. Exemple : `2*x + 5*y ≤ 10`. + +--- + +## Points Importants du Code + +1. **Gestion des Identifiants** : +- Les identifiants spécifiques au tas (`heap`, `this`, etc.) sont ignorés dans les mises à jour. + +2. **Gestion des Assumptions et Simulations Étape par Étape** : +- Les hypothèses non linéaires ou hors domaine ne modifient pas l'état actuel. + +3. **Représentation en String** : +- Les inéquations sont affichées dans une syntaxe proche de la mathématique classique, facilitant la lecture des sorties du domaine. + +4. **Support Étendu pour le Domaine Relationnel** : +- Les méthodes génériques comme `lub`, `glb`, et `satisfies` permettent de manipuler efficacement les relations au sein du domaine lors des analyses programmatiques. + +--- + +## Cas d'Application + +### Exemples : +#### 1. Expression Simple : +```java +x = z + 5; +y = x + 3; +``` +Cela se traduit par l'ajout des inéquations suivantes : +- `x - z <= 5` +- `y - x <= 3` + +#### 2. Hypothèses Conditionnelles : +```java +if ((1*x + 5*y) <= 4) { ... } +``` +L'analyse gère ce type d'expression en stockant la contrainte `(1*x + 5*y) <= 4` comme une inéquation linéaire. + +#### 3. Simplification via Transitivité : +Given : +- Relation 1 : `x + y ≤ 3` +- Relation 2 : `y - z ≤ 5` + +Les deux relations produisent transitivement une autre inéquation : `x - z ≤ 8`. + +--- + +## **Résumé** +Le domaine `TwoVariablesInequalityDomain` fournit une base puissante pour analyser des systèmes simples d'inéquations linéaires avec deux variables. Il s’intègre bien dans des analyses plus globales grâce à ses capacités de simplification et de fermeture transitives. +Il est quand même encore possible d'élargir davantage les instructions couvertes par cette implementation (ex: en tenant compte toutes les autres inégalités) + +--- + +# Produit Cartésien de Domaines + +traite de l'analyse basée sur **le produit cartésien** entre deux domaines, : + +--- + +### Classe Principale : `IntervalSafeOverflowTwoVariablesInequalityCartesianProduct.java` +### Classe Test : `IntervalSafeOveflowAndLinearInequalityCartesianProductTest.java` +### Input : `ProduitCartesian.imp` + +--- +``` +basic_linear(){ + def x = -1; + def z = 2; + def u = 6; + u = z - 2; + def y = x + 5; +} +``` + +## Contexte : Le Produit Cartésien +L'approche implémentée repose sur la combinaison de deux domaines principaux : +1. **Domaine des Inéquations Linéaires à Deux Variables** : Suit et interprète des relations telles que `ax + by ≤ c`. +2. **Domaine des Intervalles** : Fournit des informations numériques précises sur les bornes des variables pour éviter les débordements, grâce au domaine `IntervalSafeOverflowDomain`. + +Le **produit cartésien** combine ces deux domaines pour analyser des relations complexes tout en validant ou invalidant les contraintes en projetant des intervalles dans les inéquations. + +--- + +## Fonctionnalité Clé : Réduction via le Produit Cartésien +La réduction consiste à croiser les informations des deux domaines pour valider ou invalider les relations définies entre les variables. Voici un résumé des étapes principales : + +1. ***Extraction des contraintes relationnelles*** : +- Les inégalités du domaine linéaire sont analysées. + +2. ***Projection des intervalles*** : +- Les bornes des variables issues des intervalles sont multipliées par leurs coefficients dans chaque inégalité. +- Les bornes minimales (`min`) et maximales (`max`) pour chaque inégalité sont calculées en combinant les projections. + +3. ***Vérification des contradictions*** : +- Une inégalité est validée si ses valeurs projetées respectent la contrainte (par exemple, `max ≤ c`, où `c` est la constante de l’inégalité). +- En cas de contradiction, les variables impliquées sont mises sur **TOP**. + +--- + +## Application au Code fourni + +Examinons le code `basic_linear()` avec cette approche. + +### Étape 1 : Compilation des Contraintes et Intervalles +Voici les informations initiales extraites des deux domaines : + +| **Variable** | **Expression** | **Intervalle (Bornes)** | **Inéquation (Relations issues du domaine)** | +|--------------|--------------------------|-------------------------------|-------------------------------------------| +| `x` | `-1` | `[-1, -1]` | TOP | +| `z` | `2` | `[2, 2]` | TOP | +| `u` | `6` | `[6, 6]` | TOP | +| `u` | `z - 2` | `2 - 2 = 0` | `u - z ≤ -2` | +| `y` | `x + 5` | `(-1) + 5 = [4, 4]` | `y - x ≤ 5` | + +Les environnements finaux seront +`{ y - x <= 5 , u - z <= -2 }` +et +`u`: `[0 .. 0]`, +`x`: `[-1 .. -1]`, +`y`: `[4 .. 4]`, +`z`: `[2 .. 2]` + +--- + +### Étape 2 : Vérification et Réduction + +#### **Inégalité 1 : `u - z ≤ -2`** +- **Calcul Projeté :** + - Intervalle de `u` : `[6, 6]` + - Intervalle de `z` : `[2, 2]` + - Coefficient de `u` : `1` + - Coefficient de `z` : `-1` + - Projections : + ``` + u : [+1 * 6, +1 * 6] = [6, 6] + z : [-1 * 2, -1 * 2] = [-2, -2] + min = 6 + (-2) = 4 + max = 6 + (-2) = 4 + ``` +- **Résultat :** + - La borne maximale projetée (`4`) ne respecte pas la contrainte attendue (`max ≤ -2`). +- **Action attendue :** + - Une contradiction est détectée pour `u - z ≤ -2` : les variables `u` et `z` doivent être mises sur **TOP** dans le domaine des intervalles. + +#### **Inégalité 2 : `y - x ≤ 5`** +- **Calcul Projeté :** + - Intervalle de `y` : `[4, 4]` + - Intervalle de `x` : `[-1, -1]` + - Coefficient de `y` : `1` + - Coefficient de `x` : `-1` + - Projections : + ``` + y : [+1 * 4, +1 * 4] = [4, 4] + x : [-1 * -1, -1 * -1] = [1, 1] + min = 4 + 1 = 5 + max = 4 + 1 = 5 + ``` +- **Résultat :** + - La borne maximale projetée (`5`) respecte bien la contrainte attendue (`max ≤ 5`). + - L'inégalité est valide. + +--- + +### Étape 3 : Résultat attendu après Réduction +Après la réduction, les domaines devraient être transformés comme suit : + +#### **Domaine Relationnel (Inéquations)** : +- `u - z ≤ -2` : Contradiction détectée, remplacée par la mise des variables sur **TOP**. +- `y - x ≤ 5` : Validée, restée inchangée. + +#### **Domaine Intervallaire (Bornes)** : +- `x ∈ [-1, -1]` +- `z ∈ TOP` *(en raison de la contradiction)* +- `u ∈ TOP` *(en raison de la contradiction)* +- `y ∈ [4, 4]` + +--- + +## Limitation du Code Actuel + +### Comportement Observé dans le Code Actuel +Dans le code, la logique de projection et de vérification des inégalités (`reduce`) est correctement mise en œuvre pour identifier les contradictions. Cependant, **le code ne met pas correctement à jour les variables avec l'état abstrait TOP (`newRight.putState`) lorsqu'une contradiction est détectée**. + +### Ajustement Nécessaire +Pour que le processus de réduction fonctionne comme prévu : +1. Lorsqu'une contradiction est identifiée, il faut assurer que toutes les variables impliquées dans l'inégalité contradictoire soient mises sur TOP, comme indiqué dans cette section : + ```java + if (!isValid) { + System.out.println("Contradiction detected for inequality: " + linearInequality); + + // Si l'inégalité est invalide, mettre toutes ses variables sur TOP + for (Identifier variable : variableCoefficientsMap.keySet()) { + System.out.println("Setting variable " + variable + " to TOP due to invalid inequality."); + newRight = newRight.putState(variable, new IntervalSafeOverflowDomain().top()); + } + } + ``` +2. S'assurer que `newRight` soit effectivement mis à jour dans l'objet final créé à la fin de la méthode `reduce`. + +L'absence de cette mise à jour provoque une incohérence entre l'analyse conceptuelle et les résultats réellement retournés par l'analyse. + +--- + +## **Résumé** +Le **produit cartésien** proposé combine efficacement les domaines relationnel et intervallaire pour : +1. Détecter des contradictions en projetant les intervalles dans les relations linéaires. +2. Gérer les imprécisions en utilisant l'état abstrait TOP. + +### Résultat Attendu +Pour le code `basic_linear()` : +- `x ∈ [-1, -1]` +- `z ∈ TOP` *(en raison de la contradiction dans `u - z ≤ -2`)* +- `u ∈ TOP` *(en raison de la contradiction dans `u - z ≤ -2`)* +- `y ∈ [4, 4]` + +### Modification Nécessaire +L'algorithme **doit être ajusté pour profiter de la communication des 2 domaines et garantir la mise à jour des variables en TOP** lors d'une contradiction, comme décrit dans la section des ajustements nécessaires. + +Une fois cette correction apportée, l'analyse produira les résultats attendus et permettra une utilisation correcte dans des scénarios plus complexes. \ No newline at end of file diff --git a/inputs/ProduitCartesien.imp b/inputs/ProduitCartesien.imp new file mode 100644 index 0000000..096c739 --- /dev/null +++ b/inputs/ProduitCartesien.imp @@ -0,0 +1,11 @@ +class ProduitCartesien { + + basic_linear(){ + def x = -1; + def z = 2; + def u = 6; + u = z - 2; + def y = x + 5; + } + +} \ No newline at end of file diff --git a/inputs/TwoVariablesInequality.imp b/inputs/TwoVariablesInequality.imp new file mode 100644 index 0000000..d2da510 --- /dev/null +++ b/inputs/TwoVariablesInequality.imp @@ -0,0 +1,35 @@ +class twovariablesinequality { + + basic(){ + def x = 0; + def z = 1; + def u = z - 2; + def y = x + 5; + if((2*x+5*y) <= 3){ + def w=3; + } + } + + applyClosureAndTransitivity(){ + def x = 0; + def z = 1; + def y = x + 5; + y = x + 3; + x = z + 5; + } + + condition(){ + def a = 1; + def b = 7; + def x = 1; + def y = 1; + + if((1*x + 5*y) <= 4){ + def z=2; + } + else { + if((2*x + 4*y) <= 5) + def z=3; + } + } +} \ No newline at end of file diff --git a/inputs/intervalleSafeOverflow.imp b/inputs/intervalleSafeOverflow.imp new file mode 100644 index 0000000..1485c67 --- /dev/null +++ b/inputs/intervalleSafeOverflow.imp @@ -0,0 +1,67 @@ +class intervalleSafeOverflow { + basic() { + def i = 2147483647; + def j = 20; + def k = -j; + def a = i + j; + def s = i - j; + def m = i * j; + def d = i / j; + } + + whilestatement() { + def a = -2; + def x = 0; + while(a>=1) + x = x + 2; + } + + wideningwhilestatement() { + def a = 0; + def x = 1; + while(a<=10) { + x = x * 2; + a = a + 1; + } + } + + ifstatement() { + def i = 0; + if(i > 0) + i = 1; + else + def j = i * 2; + } + + /*severalvalues() { + def i = 0; + def j = 1; + if(i > 1) { + i = 1; + j = 2; + } + if(i > 1) { + i = i+1; + j = j+2; + } + + if(i > 1) { + i = i+1; + j = j+2; + } + if(i > 1) { + i = i+1; + j = j+2; + } + if(i > 1) { + i = i+1; + j = j+2; + } + if(i > 1) { + i = i+1; + j = j+2; + } + def a = i + j; + + }*/ +} \ No newline at end of file diff --git a/src/main/java/it/unive/lisa/tutorial/IntervalSafeOverflowDomain.java b/src/main/java/it/unive/lisa/tutorial/IntervalSafeOverflowDomain.java new file mode 100644 index 0000000..8957df7 --- /dev/null +++ b/src/main/java/it/unive/lisa/tutorial/IntervalSafeOverflowDomain.java @@ -0,0 +1,489 @@ +package it.unive.lisa.tutorial; + +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.value.Constant; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.ValueExpression; +import it.unive.lisa.symbolic.value.operator.AdditionOperator; +import it.unive.lisa.symbolic.value.operator.DivisionOperator; +import it.unive.lisa.symbolic.value.operator.MultiplicationOperator; +import it.unive.lisa.symbolic.value.operator.SubtractionOperator; +import it.unive.lisa.symbolic.value.operator.binary.*; +import it.unive.lisa.symbolic.value.operator.unary.NumericNegation; +import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; + +import java.util.Arrays; + +/** + * A non-relational abstract domain representing intervals with floating-point rounding. + * Each variable is mapped to an interval [low, high], adjusted for rounding errors. + */ +public class IntervalSafeOverflowDomain implements BaseNonRelationalValueDomain { + + public static final IntervalSafeOverflowDomain TOP = new IntervalSafeOverflowDomain(IntOrInf.infiniteNeg, IntOrInf.infinitePos); + public static final IntervalSafeOverflowDomain BOTTOM = new IntervalSafeOverflowDomain(IntOrInf.infinitePos, IntOrInf.infiniteNeg); + + public static final int MIN = Integer.MIN_VALUE; + public static final int MAX = Integer.MAX_VALUE; + + + private final IntOrInf low; + + + private final IntOrInf high; + + public IntOrInf getLow() { + return low; + } + + public IntOrInf getHigh() { + return high; + } + // Constructor for an interval [low, high] + public IntervalSafeOverflowDomain(IntOrInf low, IntOrInf high) { + this.low = low; + this.high = high; + } + + public IntervalSafeOverflowDomain() { + this(IntOrInf.infinitePos, IntOrInf.infiniteNeg); // Invalid interval for bottom + } + + @Override + public IntervalSafeOverflowDomain top() { + return TOP; + } + + @Override + public IntervalSafeOverflowDomain bottom() { + return BOTTOM; + } + + @Override + public boolean isTop() { + return low.isNegativeInfinite() && high.isPositiveInfinite(); + } + + @Override + public boolean isBottom() { + return low.isPositiveInfinite() || high.isNegativeInfinite() || (!low.isInfinite() && !high.isInfinite() && low.value > high.value); + } + + // class for representing Int or infinity + public static class IntOrInf { + private final boolean isInf; + private final boolean isNeg; // True if negative infinity, false if positive infinity + private final int value; + public static final IntOrInf infiniteNeg = new IntOrInf(true); + public static final IntOrInf infinitePos = new IntOrInf(false); + + // Constructor for finite value + public IntOrInf(int value) { + this.isInf = false; + this.isNeg = false; + this.value = value; + } + + // Constructor for infinity + private IntOrInf(boolean isNeg) { + this.isInf = true; + this.isNeg = isNeg; + this.value = isNeg ? MIN : MAX; + } + + public boolean isInfinite() { + return isInf; + } + + public boolean isNegativeInfinite() { + return isInf && isNeg; + } + + public boolean isPositiveInfinite() { + return isInf && !isNeg; + } + + private boolean isZero() { + return value == 0 && !this.isInfinite(); + } + + private boolean isPositive() { + return value > 0 && !this.isInfinite(); + } + + private boolean isNegative() { + return value < 0 && !this.isInfinite(); + } + + public static IntOrInf min(IntOrInf a, IntOrInf b) { + if (a.isNegativeInfinite() || b.isNegativeInfinite()) return infiniteNeg; + if (a.isPositiveInfinite()) return b; + if (b.isPositiveInfinite()) return a; + return new IntOrInf(Math.min(a.value, b.value)); + } + + public static IntOrInf min(IntOrInf... values) { + return Arrays.stream(values).reduce(IntOrInf::min).orElse(infiniteNeg); + } + + public static IntOrInf max(IntOrInf a, IntOrInf b) { + if (a.isPositiveInfinite() || b.isPositiveInfinite()) return infinitePos; + if (a.isNegativeInfinite()) return b; + if (b.isNegativeInfinite()) return a; + return new IntOrInf(Math.max(a.value, b.value)); + } + + public static IntOrInf max(IntOrInf... values) { + return Arrays.stream(values).reduce(IntOrInf::max).orElse(infinitePos); + } + + public static IntOrInf add(IntOrInf a, IntOrInf b) { + if (a.isInfinite() || b.isInfinite()) { + if (a.isNegativeInfinite() || b.isNegativeInfinite()) return infiniteNeg; + return infinitePos; + } + + long result = (long) a.value + (long) b.value; + return new IntOrInf(handleOverflow(result)); + } + + public static IntOrInf sub(IntOrInf a, IntOrInf b) { + if (a.isInfinite() || b.isInfinite()) { + if (a.isNegativeInfinite() || b.isPositiveInfinite()) return infiniteNeg; + if (a.isPositiveInfinite() || b.isNegativeInfinite()) return infinitePos; + } + + long result = (long) a.value - (long) b.value; + return new IntOrInf(handleOverflow(result)); + } + + public static IntOrInf mul(IntOrInf a, IntOrInf b) { + // Cas où l'un des opérandes est zéro + if (a.isZero() || b.isZero()) { + if (a.isInfinite() || b.isInfinite()) { + throw new ArithmeticException("Multiplication indéfinie : 0 * ∞"); + } + return new IntOrInf(0); + } + + // Cas où les deux opérandes sont infinis + if (a.isInfinite() && b.isInfinite()) { + if (a.isNegativeInfinite() == b.isNegativeInfinite()) { + return infinitePos; // (-∞) * (-∞) = ∞ et ∞ * ∞ = ∞ + } else { + return infiniteNeg; // (-∞) * ∞ = -∞ et ∞ * (-∞) = -∞ + } + } + + // Cas où un seul des opérandes est infini + if (a.isInfinite()) { + return (b.value < 0) ? (a.isPositiveInfinite() ? infiniteNeg : infinitePos) : a; + } + if (b.isInfinite()) { + return (a.value < 0) ? (b.isPositiveInfinite() ? infiniteNeg : infinitePos) : b; + } + + // Multiplication normale entre deux nombres finis + long result = (long) a.value * (long) b.value; + return new IntOrInf(handleOverflow(result)); + } + + public static IntOrInf div(IntOrInf a, IntOrInf b) { + if (b.isZero()) throw new ArithmeticException("Division par zéro !"); + if (a.isInfinite() || b.isInfinite()) { + if (a.isPositiveInfinite() && b.isPositive()) return infinitePos; + if (a.isPositiveInfinite() && b.isNegative()) return infiniteNeg; + if (a.isNegativeInfinite() && b.isPositive()) return infiniteNeg; + if (a.isNegativeInfinite() && b.isNegative()) return infinitePos; + return infinitePos; // Cas où b tend vers zéro + } + return new IntOrInf(a.value / b.value); + } + + private static int handleOverflow(long value) { + if (value > MAX) return MIN + (int) (value - MAX - 1); + if (value < MIN) return MAX - (int) (MIN - value - 1); + return (int) value; + } + + public static IntOrInf negate(IntOrInf a) { + if (a.isNegativeInfinite()) return infinitePos; + if (a.isPositiveInfinite()) return infiniteNeg; + return new IntOrInf(-a.value); + } + + public boolean lessThan(IntOrInf other) { + if (this.isNegativeInfinite()) return !other.isNegativeInfinite(); + if (this.isPositiveInfinite()) return false; + if (other.isNegativeInfinite()) return false; + if (other.isPositiveInfinite()) return true; + return this.value < other.value; + } + + public boolean lessOrEqual(IntOrInf other) { + if (this.isNegativeInfinite()) return true; + if (this.isPositiveInfinite()) return other.isPositiveInfinite(); + if (other.isNegativeInfinite()) return false; + if (other.isPositiveInfinite()) return true; + return this.value <= other.value; + } + + @Override + public String toString() { + if (isNegativeInfinite() || (value==MIN && !this.isInfinite())) return "-∞"; + if (isPositiveInfinite() || (value==MAX && !this.isInfinite())) return "+∞"; + return String.valueOf(value); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) return true; + if (!(obj instanceof IntOrInf)) return false; + IntOrInf other = (IntOrInf) obj; + if (this.isInf && other.isInf) return this.isNeg == other.isNeg; + if (this.isInf || other.isInf) return false; + return this.value == other.value; + } + + @Override + public int hashCode() { + return isInf ? (isNeg ? -1 : 1) : Double.hashCode(value); + } + } + + @Override + public IntervalSafeOverflowDomain lubAux(IntervalSafeOverflowDomain other) throws SemanticException { + if (this.isBottom() || other.isBottom()) return bottom(); + return new IntervalSafeOverflowDomain(IntervalSafeOverflowDomain.IntOrInf.min(this.low, other.low), IntervalSafeOverflowDomain.IntOrInf.max(this.high, other.high)); + } + + @Override + public IntervalSafeOverflowDomain glbAux(IntervalSafeOverflowDomain other) throws SemanticException { + if (this.isBottom() || other.isBottom()) return BOTTOM; + IntOrInf newLow = IntOrInf.max(this.low, other.low); + IntOrInf newHigh = IntOrInf.min(this.high, other.high); + return newLow.lessOrEqual(newHigh) ? new IntervalSafeOverflowDomain(newLow, newHigh) : BOTTOM; + } + + @Override + public IntervalSafeOverflowDomain wideningAux(IntervalSafeOverflowDomain other) throws SemanticException { + System.out.println(this.isBottom()); + if (this.isBottom()) return other; + if (other.isBottom()) return this; + IntOrInf newLow = other.low.lessThan(this.low) ? IntOrInf.infiniteNeg : this.low; + IntOrInf newHigh = this.high.lessThan(other.high) ? IntOrInf.infinitePos : this.high; + return new IntervalSafeOverflowDomain(newLow, newHigh); + } + + @Override + public boolean lessOrEqualAux(IntervalSafeOverflowDomain other) throws SemanticException { + if (this.isBottom()) return true; + if (other.isBottom()) return false; + return other.low.lessOrEqual(this.low) && this.high.lessOrEqual(other.high); + } + + @Override + public IntervalSafeOverflowDomain evalNullConstant(ProgramPoint pp, SemanticOracle oracle) throws SemanticException { + return TOP; + } + + @Override + public IntervalSafeOverflowDomain evalNonNullConstant(Constant constant, ProgramPoint pp, SemanticOracle oracle) throws SemanticException { + if (constant.getValue() instanceof Number) { + int val = (int) constant.getValue(); + return new IntervalSafeOverflowDomain(new IntOrInf(val), new IntOrInf(val)); + } + return TOP; + } + + @Override + public IntervalSafeOverflowDomain evalUnaryExpression(UnaryOperator operator, IntervalSafeOverflowDomain arg, ProgramPoint pp, SemanticOracle oracle) throws SemanticException { + if (arg.isBottom()) return BOTTOM; + if (operator == NumericNegation.INSTANCE) { + return new IntervalSafeOverflowDomain(IntOrInf.negate(arg.high), IntOrInf.negate(arg.low)); + } + return TOP; + } + + @Override + public IntervalSafeOverflowDomain evalBinaryExpression(BinaryOperator operator, IntervalSafeOverflowDomain left, IntervalSafeOverflowDomain right, ProgramPoint pp, SemanticOracle oracle) throws SemanticException { + System.out.println(left + " " + operator +" " + right); + if (left.isBottom() || right.isBottom()) return BOTTOM; + if (operator instanceof AdditionOperator) { + IntOrInf low = IntOrInf.add(left.low, right.low); + IntOrInf high = IntOrInf.add(left.high, right.high); + return new IntervalSafeOverflowDomain(low, high); + } else if (operator instanceof SubtractionOperator) { + IntOrInf low = IntOrInf.sub(left.low, right.high); + IntOrInf high = IntOrInf.sub(left.high, right.low); + return new IntervalSafeOverflowDomain(low, high); + } else if (operator instanceof MultiplicationOperator) { + IntOrInf[] bounds = { + IntOrInf.mul(left.low, right.low), IntOrInf.mul(left.low, right.high), + IntOrInf.mul(left.high, right.low), IntOrInf.mul(left.high, right.high) + }; + IntOrInf low = IntOrInf.min(Arrays.stream(bounds).toArray(IntOrInf[]::new)); + IntOrInf high = IntOrInf.max(Arrays.stream(bounds).toArray(IntOrInf[]::new)); + return new IntervalSafeOverflowDomain(low, high); + } else if (operator instanceof DivisionOperator) { + if (right.low.isZero() || right.high.isZero()) { + throw new SemanticException("Division par zéro détectée !"); + } + + IntOrInf[] bounds = { + IntOrInf.div(left.low, right.low), IntOrInf.div(left.low, right.high), + IntOrInf.div(left.high, right.low), IntOrInf.div(left.high, right.high) + }; + + IntOrInf low = IntOrInf.min(bounds); + IntOrInf high = IntOrInf.max(bounds); + + return new IntervalSafeOverflowDomain(low, high); + } + + return TOP; + } + + @Override + public StructuredRepresentation representation() { + if (isBottom()) return new StringRepresentation(Lattice.BOTTOM_STRING); + if (isTop()) return new StringRepresentation(Lattice.TOP_STRING); + return new StringRepresentation("[" + low + " .. " + high + "]"); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) return true; + if (!(obj instanceof IntervalSafeOverflowDomain)) return false; + IntervalSafeOverflowDomain other = (IntervalSafeOverflowDomain) obj; + return this.low.equals(other.low) && this.high.equals(other.high); + } + + @Override + public int hashCode() { + return low.hashCode() * 31 + high.hashCode(); + } + + public Integer getMin() { + if(low.isInfinite()) return null; + else return low.value; + } + + public Integer getMax() { + if(high.isInfinite()) return null; + else return high.value; + } + + @Override + public String toString() { + if (isBottom()) return "BOTTOM"; + if (isTop()) return "TOP"; + if (low.value == Integer.MIN_VALUE && high.value == Integer.MAX_VALUE) { + return "[ -∞ .. +∞ ]"; + } + if (low.value == Integer.MIN_VALUE) { + return "[ -∞ .. " + high + "]"; + } + if (high.value == Integer.MAX_VALUE) { + return "[" + low + " .. +∞ ]"; + } + return "[" + low + " .. " + high + "]"; + } + + @Override + public ValueEnvironment assumeBinaryExpression( + ValueEnvironment environment, + BinaryOperator operator, + ValueExpression left, + ValueExpression right, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + + Identifier id; + IntervalSafeOverflowDomain eval; + boolean rightIsExpr; + + // Étape 1 : Identifier la variable et évaluer l'autre opérande + if (left instanceof Identifier) { + eval = eval(right, environment, src, oracle); + id = (Identifier) left; + rightIsExpr = true; + } else if (right instanceof Identifier) { + eval = eval(left, environment, src, oracle); + id = (Identifier) right; + rightIsExpr = false; + } else { + System.out.println("assumeBinary: neither left nor right is an identifier, returning unchanged environment"); + return environment; // Ni left ni right n'est un identifiant, pas de raffinement + } + + // Étape 2 : Récupérer l'intervalle actuel de la variable + IntervalSafeOverflowDomain starting = environment.getState(id); + + if (eval.isBottom() || starting.isBottom()) { + return environment.bottom(); + } + + if (operator instanceof ComparisonEq) { + // a == 1 -> a: [1 .. 1] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(eval.low.value), new IntOrInf(eval.high.value))); + } else if (operator instanceof ComparisonGe) { + if (rightIsExpr) { + // a >= 1 -> a: [1, +∞] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(eval.getMax()), new IntOrInf(false))); + } else { + // 1 >= a -> a: [-∞, 1] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(true), new IntOrInf(eval.getMin()))); + } + } else if (operator instanceof ComparisonGt) { + if (rightIsExpr) { + // a > 1 -> a: [1 + 1, +∞] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(eval.getMax()+1), new IntOrInf(false))); + } else { + // 1 > a -> a: [-∞, 1 - 1] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(true), new IntOrInf(eval.getMin()-1))); + } + } else if (operator instanceof ComparisonLe) { + if (rightIsExpr) { + // a <= 1 -> a: [-∞, 1] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(true), new IntOrInf(eval.getMin()))); + } else { + // 1 <= a -> a: [1, +∞] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(eval.getMax()), new IntOrInf(false))); + } + } else if (operator instanceof ComparisonLt) { + if (rightIsExpr) { + // a < 1 -> a: [-∞, 1 - 1] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(true), new IntOrInf(eval.getMin()-1))); + } else { + // 10 < i -> i: [1 + 1, +∞] + return environment.putState(id, new IntervalSafeOverflowDomain(new IntOrInf(eval.getMax()+1), new IntOrInf(false))); + } + } + + return BaseNonRelationalValueDomain.super.assumeBinaryExpression(environment, operator, left, right, src, dest, oracle); + } + + public IntervalSafeOverflowDomain adjustUpperBound(IntOrInf upperLimit) { + if (upperLimit.lessThan(this.low)) { + return BOTTOM; // Contradiction si la borne supérieure est plus basse que la borne inférieure actuelle + } + return new IntervalSafeOverflowDomain(this.low, IntOrInf.min(this.high, upperLimit)); + } + + public IntervalSafeOverflowDomain adjustLowerBound(IntOrInf lowerLimit) { + if (lowerLimit.lessThan(this.high)) { + return BOTTOM; // Contradiction si la borne inférieure dépasse la borne supérieure + } + return new IntervalSafeOverflowDomain(IntOrInf.max(this.low, lowerLimit), this.high); + } +} \ No newline at end of file diff --git a/src/main/java/it/unive/lisa/tutorial/IntervalSafeOverflowTwoVariablesInequalityCartesianProduct.java b/src/main/java/it/unive/lisa/tutorial/IntervalSafeOverflowTwoVariablesInequalityCartesianProduct.java new file mode 100644 index 0000000..158bbb9 --- /dev/null +++ b/src/main/java/it/unive/lisa/tutorial/IntervalSafeOverflowTwoVariablesInequalityCartesianProduct.java @@ -0,0 +1,119 @@ +package it.unive.lisa.tutorial; + +import it.unive.lisa.analysis.combination.CartesianProduct; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.analysis.value.ValueDomain; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.ValueExpression; + +import java.util.Map; + +public class IntervalSafeOverflowTwoVariablesInequalityCartesianProduct extends CartesianProduct,ValueExpression,Identifier> + implements ValueDomain +{ + public IntervalSafeOverflowTwoVariablesInequalityCartesianProduct(TwoVariablesInequalityDomain left, ValueEnvironment right) { + super(left, right); + } + @Override + public boolean knowsIdentifier(Identifier id) { + return left.knowsIdentifier(id) || right.knowsIdentifier(id); + } + + @Override + public IntervalSafeOverflowTwoVariablesInequalityCartesianProduct mk(TwoVariablesInequalityDomain left, ValueEnvironment right) { + return new IntervalSafeOverflowTwoVariablesInequalityCartesianProduct(left, right).reduce(); + } + + private IntervalSafeOverflowTwoVariablesInequalityCartesianProduct reduce() { + TwoVariablesInequalityDomain newLeft = this.left; // Domain contenant les inégalités (left) + ValueEnvironment newRight = this.right; // Domain contenant les intervalles (right) + + System.out.println("Reducing"); + System.out.println("Inequalities (Left): " + newLeft); + System.out.println("Intervals (Right): " + newRight); + + // Parcourir les inégalités dans `newLeft.linearInequalities` + for (TwoVariablesInequalityDomain.LinearInequality linearInequality : newLeft.linearInequalities) { + System.out.println("Processing inequality: " + linearInequality); + + // Extraire les variables présentes dans l'inégalité avec leurs coefficients + Map variableCoefficientsMap = linearInequality.variableCoefficientsMap; + int constant = linearInequality.getConstant(); // La constante à droite de l'inégalité + + // Initialiser les bornes pour l'inégalité accumulée + int min = 0; // Minimum global (après projection des intervalles) + int max = 0; // Maximum global (après projection des intervalles) + boolean isValid = true; // Suppose que l'inégalité est valide jusqu'à preuve du contraire + + // Parcourir chaque variable et ses coefficients dans l'inégalité + for (Map.Entry entry : variableCoefficientsMap.entrySet()) { + Identifier variable = entry.getKey(); // La variable (par exemple: u, z, y, etc.) + int coefficient = entry.getValue(); // Le coefficient devant cette variable (ex: a pour ax) + + // Obtenir l'intervalle de la variable depuis `newRight` + IntervalSafeOverflowDomain interval = newRight.getState(variable); + + if (interval != null) { + // Calculer les intervalles projetés pour cette variable + System.out.println("Variable: " + variable + ", Coefficient: " + coefficient + ", Interval: " + interval); + + int projectedMin = coefficient * interval.getMin(); + int projectedMax = coefficient * interval.getMax(); + + // Additionner les bornes projetées dans les bornes globales + if (coefficient > 0) { + min += projectedMin; + max += projectedMax; + } else { + // Les bornes inversées si le coefficient est négatif + min += projectedMax; + max += projectedMin; + } + } else { + // Intervalle manquant dans `right` -> Mettre cette variable sur TOP + System.out.println("Interval missing for variable: " + variable + ", setting to TOP."); + newRight = newRight.putState(variable, new IntervalSafeOverflowDomain().top()); + isValid = false; // L'inégalité devient invalide si l'intervalle est manquant + } + } + + // Vérification de l'inégalité avec les bornes globales accumulées + if (isValid) { + isValid = checkLinearInequality(linearInequality, min, max); + } + + if (!isValid) { + System.out.println("Contradiction detected for inequality: " + linearInequality); + + // Si l'inégalité est invalide, toutes ses variables sont mises sur TOP + for (Identifier variable : variableCoefficientsMap.keySet()) { + System.out.println("Setting variable " + variable + " to TOP due to invalid inequality."); + newRight = newRight.putState(variable, new IntervalSafeOverflowDomain().top()); + } + } + } + + return new IntervalSafeOverflowTwoVariablesInequalityCartesianProduct(newLeft, newRight); + } + + /** + * Vérifie si une inégalité avec des bornes projetées est valide. + * + * @param linearInequality L'inégalité initiale + * @param min La borne minimale accumulée + * @param max La borne maximale accumulée + * @return true si l'inégalité est valide, false sinon + */ + private boolean checkLinearInequality(TwoVariablesInequalityDomain.LinearInequality linearInequality, int min, int max) { + int constant = linearInequality.getConstant(); // La constante à droite de l'inégalité + boolean isLessOrEqual = linearInequality.isLessOrEqualConstraint; // Type de contrainte + + if (isLessOrEqual) { + // Vérifier si les limites respectent <= + return max <= constant; + } else { + // Vérifier si les limites respectent < + return max < constant; + } + } +} \ No newline at end of file diff --git a/src/main/java/it/unive/lisa/tutorial/TwoVariablesInequalityDomain.java b/src/main/java/it/unive/lisa/tutorial/TwoVariablesInequalityDomain.java new file mode 100644 index 0000000..ec4bb36 --- /dev/null +++ b/src/main/java/it/unive/lisa/tutorial/TwoVariablesInequalityDomain.java @@ -0,0 +1,594 @@ +package it.unive.lisa.tutorial; + +import java.util.*; +import java.util.function.Predicate; + +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.ScopeToken; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; +import it.unive.lisa.analysis.value.ValueDomain; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.SymbolicExpression; +import it.unive.lisa.symbolic.value.BinaryExpression; +import it.unive.lisa.symbolic.value.Constant; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.ValueExpression; +import it.unive.lisa.symbolic.value.operator.AdditionOperator; +import it.unive.lisa.symbolic.value.operator.MultiplicationOperator; +import it.unive.lisa.symbolic.value.operator.SubtractionOperator; +import it.unive.lisa.symbolic.value.operator.binary.ComparisonLe; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; + +public class TwoVariablesInequalityDomain implements ValueDomain { + public static final TwoVariablesInequalityDomain TOP = new TwoVariablesInequalityDomain(true); + public static final TwoVariablesInequalityDomain BOTTOM = new TwoVariablesInequalityDomain(false); + public Set linearInequalities = new HashSet<>(); + + private static final String HEAP_IDENTIFIER = "heap"; + private static final String THIS_IDENTIFIER = "this"; + private static final String PP_IDENTIFIER = "&pp@"; + + public boolean isTopDomain = false, isBottomDomain = false; + + private TwoVariablesInequalityDomain(boolean isTopDomain) { + if (isTopDomain) + this.isTopDomain = true; + else + this.isBottomDomain = true; + this.linearInequalities = new HashSet<>(); + } + + // constructor + public TwoVariablesInequalityDomain(Set inequalities) { + if (inequalities.isEmpty()) + this.isTopDomain = true; + this.linearInequalities = new HashSet<>(processAndSimplifyLinearInequalities(inequalities)); + } + + public TwoVariablesInequalityDomain top() { + return TOP; + } + + public boolean isTop() { + return this.isTopDomain; + } + + public boolean isBottom() { + return this.isBottomDomain; + } + + public TwoVariablesInequalityDomain bottom() { + return BOTTOM; + } + + public boolean knowsIdentifier(Identifier id) { + return false; + } + + public TwoVariablesInequalityDomain forgetIdentifiersIf(Predicate condition) throws SemanticException { + return this; + } + + public TwoVariablesInequalityDomain pushScope(ScopeToken scope) throws SemanticException { + return this; + } + + public TwoVariablesInequalityDomain popScope(ScopeToken scope) throws SemanticException { + return this; + } + + public StructuredRepresentation representation() { + if (isTop()) + return new StringRepresentation(Lattice.TOP_STRING); + if (isBottom()) + return new StringRepresentation(Lattice.BOTTOM_STRING); + return new StringRepresentation(toString()); + } + + /** + * Processes the assumption of a binary value expression in the domain of + * two-variable inequalities. Updates the current domain if the expression + * represents a comparison between variables or specific forms of binary + * expressions. If the expression is not a binary comparison or cannot be + * handled, the current domain remains unchanged. + * + * @param expr the value expression to be assumed, potentially a binary + * comparison + * @param srcPoint the program point where the assumption originates + * @param destPoint the program point where the assumption leads + * @param oracle the semantic oracle providing additional information + * about the program's semantics + * @return a new domain reflecting the assumption if it can be handled, + * or the same domain otherwise + * @throws SemanticException if an error occurs during the processing of + * the assumption + */ + @Override + public TwoVariablesInequalityDomain assume( + ValueExpression expr, + ProgramPoint srcPoint, + ProgramPoint destPoint, + SemanticOracle oracle) throws SemanticException { + + if (!(expr instanceof BinaryExpression)) { + return this; + } + + BinaryExpression binaryExpr = (BinaryExpression) expr; + + if (!(binaryExpr.getOperator() instanceof ComparisonLe)) { + return this; + } + + SymbolicExpression leftOperand = binaryExpr.getLeft(); + SymbolicExpression rightOperand = binaryExpr.getRight(); + + if (leftOperand instanceof Identifier && rightOperand instanceof Identifier) { + return processIdentifierComparison((Identifier) leftOperand, (Identifier) rightOperand); + } else if (leftOperand instanceof BinaryExpression && rightOperand instanceof Constant) { + return processComplexExpression( + (BinaryExpression) leftOperand, + (Constant) rightOperand + ); + } + + return this; + } + + private TwoVariablesInequalityDomain processIdentifierComparison(Identifier leftId, Identifier rightId) { + Map coefficientMap = new HashMap<>(); + coefficientMap.put(leftId, 1); + coefficientMap.put(rightId, -1); + + LinearInequality linearInequality = new LinearInequality(coefficientMap, 0); + Set updatedSet = createUpdatedSet(linearInequality); + + return new TwoVariablesInequalityDomain(updatedSet); + } + + private TwoVariablesInequalityDomain processComplexExpression( + BinaryExpression leftExpr, + Constant rightConstant) { + + int constantValue = (Integer) rightConstant.getValue(); + Map coefficientMap = new HashMap<>(); + + // Extraire les coefficients et variables si possible + if (leftExpr.getOperator() instanceof AdditionOperator) { + SymbolicExpression axTerm = leftExpr.getLeft(); + SymbolicExpression byTerm = leftExpr.getRight(); + + if (axTerm instanceof BinaryExpression && byTerm instanceof BinaryExpression) { + BinaryExpression axSubExpr = (BinaryExpression) axTerm; + BinaryExpression bySubExpr = (BinaryExpression) byTerm; + + if (axSubExpr.getOperator() instanceof MultiplicationOperator + && bySubExpr.getOperator() instanceof MultiplicationOperator) { + + extractCoefficientAndVariable(axSubExpr, coefficientMap); + extractCoefficientAndVariable(bySubExpr, coefficientMap); + + LinearInequality linearInequality = new LinearInequality(coefficientMap, constantValue); + Set updatedSet = createUpdatedSet(linearInequality); + + return new TwoVariablesInequalityDomain(updatedSet); + } + } + } + + return this; + } + + /** + * Extracts the coefficient and variable identifier from a given binary expression + * and updates the provided map of coefficients with the extracted data. + * The binary expression is expected to consist of a constant and an identifier. + * + * @param binaryExpression the binary expression containing the constant and identifier + * whose values are to be extracted + * @param coefficients a map associating identifiers with their corresponding coefficients, + * which will be updated with the extracted data + */ + private void extractCoefficientAndVariable( + BinaryExpression binaryExpression, + Map coefficients) { + + if (binaryExpression.getLeft() instanceof Constant && binaryExpression.getRight() instanceof Identifier) { + Constant constValue = (Constant) binaryExpression.getLeft(); + Identifier id = (Identifier) binaryExpression.getRight(); + int coefficientValue = (Integer) constValue.getValue(); + coefficients.put(id, coefficientValue); + } + } + + private Set createUpdatedSet(LinearInequality inequality) { + Set newSet = new HashSet<>(this.linearInequalities); + newSet.add(inequality); + return newSet; + } + + public static boolean isHeapIdentifier(Identifier id) { + String idString = id.toString(); + return containsIdentifier(idString, HEAP_IDENTIFIER) + || containsIdentifier(idString, THIS_IDENTIFIER) + || containsIdentifier(idString, PP_IDENTIFIER); + } + + private static boolean containsIdentifier(String idString, String identifier) { + return idString.contains(identifier); + } + + /** + * Assigns a value to a given variable within the domain of two-variable + * linear inequalities. Updates the domain to reflect the new assignment if + * applicable. If the assignment cannot be processed, the current domain + * remains unchanged. + * + * @param varId the identifier of the variable being assigned a value + * @param valueExpr the value expression representing the assigned value, + * which can be an identifier, constant, or binary expression + * @param point the program point where the assignment takes place + * @param oracle the semantic oracle providing additional information + * about program semantics + * @return a new TwoVariablesInequalityDomain reflecting the assignment if + * it is applicable, or the same domain if no update is required + * @throws SemanticException if an error occurs while processing the assignment + */ + public TwoVariablesInequalityDomain assign(Identifier varId, ValueExpression valueExpr, ProgramPoint point, + SemanticOracle oracle) throws SemanticException { + if (isHeapIdentifier(varId)) + return this; + + if (valueExpr instanceof Identifier) { + Identifier expressionId = (Identifier) valueExpr; + Map coefficientMap = new HashMap<>(); + coefficientMap.put(varId, 1); + coefficientMap.put(expressionId, -1); + LinearInequality linearInequality = new LinearInequality(coefficientMap, 0); + Set newSet = new HashSet<>(this.linearInequalities); + newSet.add(linearInequality); + + return new TwoVariablesInequalityDomain(newSet); + } + + if (valueExpr instanceof BinaryExpression) { + BinaryExpression binaryExpr = (BinaryExpression) valueExpr; + + if (binaryExpr.getOperator() instanceof AdditionOperator) { + if (binaryExpr.getRight() instanceof Constant) { + if (binaryExpr.getLeft() instanceof BinaryExpression) { + BinaryExpression leftExpr = (BinaryExpression) binaryExpr.getLeft(); + if (leftExpr.getOperator() instanceof MultiplicationOperator + && leftExpr.getLeft() instanceof Constant + && leftExpr.getRight() instanceof Identifier) { + + Constant bConst = (Constant) leftExpr.getLeft(); + Identifier yId = (Identifier) leftExpr.getRight(); + Constant cConst = (Constant) binaryExpr.getRight(); + Map coefficientMap = new HashMap<>(); + coefficientMap.put(varId, 1); + coefficientMap.put(yId, -(Integer) bConst.getValue()); + return getTwoVariablesInequalityDomain(cConst, coefficientMap); + } + } + } + + if (binaryExpr.getLeft() instanceof Identifier && binaryExpr.getRight() instanceof Constant) { + Identifier exprId = (Identifier) binaryExpr.getLeft(); + Constant constValue = (Constant) binaryExpr.getRight(); + Map coefficientMap = new HashMap<>(); + coefficientMap.put(varId, 1); + coefficientMap.put(exprId, -1); + return getTwoVariablesInequalityDomain(constValue, coefficientMap); + } + } + + if (binaryExpr.getOperator() instanceof SubtractionOperator) { + // Vérifie si c'est une soustraction de type "Identifier - Constant" + if (binaryExpr.getLeft() instanceof Identifier && binaryExpr.getRight() instanceof Constant) { + // Extraire les composants de l'expression + Identifier exprId = (Identifier) binaryExpr.getLeft(); // Par exemple, 'z' + Constant constValue = (Constant) binaryExpr.getRight(); // Par exemple, '2' + + // Création d'une nouvelle inégalité : u - z <= -2 + Map coefficientMap = new HashMap<>(); + coefficientMap.put(varId, 1); // 'u' a un coefficient de +1 + coefficientMap.put(exprId, -1); // 'z' a un coefficient de -1 + int constantC = -((Integer) constValue.getValue()); // Constante convertie avec le signe correct + + // Retournez le domaine avec cette nouvelle inégalité + return getTwoVariablesInequalityDomain(new Constant(varId.getStaticType(), constantC, point.getLocation()), coefficientMap); + } + } + } + return this; + } + + /** + * Creates a new TwoVariablesInequalityDomain by adding a linear inequality, + * defined using the provided constant value and coefficient map, to the + * existing set of inequalities. + * + * @param constVal the constant value that defines the inequality's constant term + * @param coefficientMap a map associating variable identifiers with their + * respective coefficients in the inequality + * @return a new TwoVariablesInequalityDomain containing the updated set of inequalities + */ + private TwoVariablesInequalityDomain getTwoVariablesInequalityDomain(Constant constVal, Map coefficientMap) { + LinearInequality linearInequality = new LinearInequality(coefficientMap, (Integer) (constVal.getValue())); + Set newSet = new HashSet<>(this.linearInequalities); + newSet.add(linearInequality); + + return new TwoVariablesInequalityDomain(newSet); + } + + /** + * Processes a set of linear inequalities and simplifies them by removing redundant inequalities, + * ensuring tighter bounds are retained, and deriving new inequalities based on transitivity rules. + * This method also excludes single-variable inequalities, inequalities without any variables, + * and trivial inequalities from the resulting set. + * + * @param inequalities the set of linear inequalities to be processed and simplified + * @return a simplified and processed set of linear inequalities with redundancies removed + */ + public Set processAndSimplifyLinearInequalities(Set inequalities) { + Map uniqueInequalities = new HashMap<>(); + Set toAdd = new HashSet<>(); + + for (LinearInequality inequality : inequalities) { + // Generate a key based on the variable coefficients + String key = inequality.variableCoefficientsMap.toString(); + + // Skip inequalities without any variables (e.g., y <= 6 where no variable is present) + // OR inequalities with a single variable + if (inequality.variableCoefficientsMap.isEmpty() || isSingleVariableInequality(inequality)) { + continue; + } + + // If the key already exists, update the inequality with the tighter bound + if (uniqueInequalities.containsKey(key)) { + LinearInequality existing = uniqueInequalities.get(key); + if (inequality.isLessOrEqualConstraint && existing.c > inequality.c) { + uniqueInequalities.put(key, inequality); // Keep the tighter bound + } + } else { + uniqueInequalities.put(key, inequality); + } + } + + // Transitivity check and adding derived inequalities + Set closure = new HashSet<>(uniqueInequalities.values()); + for (LinearInequality c1 : closure) { + for (LinearInequality c2 : closure) { + if (c1 != c2) { + for (Map.Entry entry : c1.variableCoefficientsMap.entrySet()) { + Identifier sharedIdentifier = entry.getKey(); + int coeff1 = entry.getValue(); + + if (c2.variableCoefficientsMap.containsKey(sharedIdentifier)) { + int coeff2 = c2.variableCoefficientsMap.get(sharedIdentifier); + if (coeff1 * coeff2 < 0 + && c1.variableCoefficientsMap.size() == 2 + && c2.variableCoefficientsMap.size() == 2) { // Ensure both inequalities involve exactly two variables + Map newCoefficients = new HashMap<>(c1.variableCoefficientsMap); + c2.variableCoefficientsMap.forEach((key, value) -> + newCoefficients.merge(key, value, Integer::sum)); + newCoefficients.remove(sharedIdentifier); + + int newConstant = c1.c + c2.c; + LinearInequality derived = new LinearInequality(newCoefficients, newConstant); + + // Ensure derived inequalities without variables, single variables, or trivial ones are discarded + if (!derived.variableCoefficientsMap.isEmpty() + && !isSingleVariableInequality(derived) + && !isTrivialInequality(derived)) { + toAdd.add(derived); + } + } + } + } + } + } + } + + closure.addAll(toAdd); + + // Remove duplicates again to prevent any leftover repetitions + Set result = new HashSet<>(); + Map finalMap = new HashMap<>(); + + for (LinearInequality inequality : closure) { + // Skip inequalities without any variables, single variable inequalities, or trivial ones + if (inequality.variableCoefficientsMap.isEmpty() || + isSingleVariableInequality(inequality) || + isTrivialInequality(inequality)) { + continue; + } + + String key = inequality.variableCoefficientsMap.toString(); + if (!finalMap.containsKey(key) || (inequality.isLessOrEqualConstraint && finalMap.get(key).c > inequality.c)) { + finalMap.put(key, inequality); + } + } + + result.addAll(finalMap.values()); + return result; + } + + // Helper method to check if an inequality contains only a single variable + private boolean isSingleVariableInequality(LinearInequality inequality) { + // An inequality is considered single-variable if it has only one coefficient + return inequality.variableCoefficientsMap.size() < 2; + } + + // Helper method to check if an inequality is trivial (same as before) + private boolean isTrivialInequality(LinearInequality inequality) { + // An inequality is trivial if all coefficients are 0 and c <= 0 + if (inequality.variableCoefficientsMap.values().stream().allMatch(coeff -> coeff == 0)) { + return inequality.c <= 0; + } + + // If there are no meaningful variable relationships, consider it trivial + return inequality.variableCoefficientsMap.size() == 1 && inequality.c <= 0; + } + + + @Override + public TwoVariablesInequalityDomain smallStepSemantics(ValueExpression valueExpr, ProgramPoint programPoint, SemanticOracle oracle) throws SemanticException { + // Handle different types of expressions + return this; + } + + @Override + public boolean lessOrEqual(TwoVariablesInequalityDomain otherDomain) throws SemanticException { + return false; + } + + /** + * Computes the least upper bound (lub) of the current domain and another + * {@code TwoVariablesInequalityDomain}. The lub represents the union of + * the sets of linear inequalities from both domains. + * + * @param otherDomain the {@code TwoVariablesInequalityDomain} to compute + * the lub with + * @return a new {@code TwoVariablesInequalityDomain} representing the + * least upper bound of the two domains + * @throws SemanticException if errors occur during the computation of the lub + */ + @Override + public TwoVariablesInequalityDomain lub(TwoVariablesInequalityDomain otherDomain) throws SemanticException { + // Return the other domain if this domain is top + if (isTop()) { + return otherDomain; + } + // Return the other domain if this domain is bottom + if (isBottom()) + return otherDomain; + // Return this domain if the other domain is top + if (otherDomain.isTop()) { + return this; + } + // Return this domain if the other domain is bottom + if (otherDomain.isBottom()) + return this; + // Create a new set that is the union of the two sets of inequalities + Set unionSet = new HashSet<>(this.linearInequalities); + unionSet.addAll(otherDomain.linearInequalities); + + return new TwoVariablesInequalityDomain(unionSet); + } + + /** + * Computes the greatest lower bound (glb) of the current domain and another + * {@code TwoVariablesInequalityDomain}. The glb represents the intersection + * of the sets of linear inequalities from both domains. + * + * @param otherDomain the {@code TwoVariablesInequalityDomain} to compute + * the glb with + * @return a new {@code TwoVariablesInequalityDomain} representing the + * greatest lower bound of the two domains + * @throws SemanticException if errors occur during the computation of the glb + */ + @Override + public TwoVariablesInequalityDomain glb(TwoVariablesInequalityDomain otherDomain) throws SemanticException { + // If the current domain is top, the greatest lower bound is the other domain + if (isTop()) return otherDomain; + + // If the other domain is top, the greatest lower bound is the current domain + if (otherDomain.isTop()) return this; + + // If either domain is bottom, the greatest lower bound is bottom + if (isBottom() || otherDomain.isBottom()) return bottom(); + + // Combine the sets of inequalities from both domains + Set result = new HashSet<>(this.linearInequalities); + result.addAll(otherDomain.linearInequalities); + + // Return the new domain containing the combined set of inequalities + return new TwoVariablesInequalityDomain(result); + } + + public String toString() { + StringBuilder result = new StringBuilder(); + result.append("{ "); + boolean isFirst = true; + + for (LinearInequality linearInequality : linearInequalities) { + if (!isFirst) result.append(" , "); + result.append(linearInequality.toString()); + isFirst = false; + } + result.append(" }"); + return result.toString(); + } + + + /** + * Class representing a linear inequality of the form ax + by ≤ c. + */ + public static class LinearInequality { + public boolean isLessOrEqualConstraint = true; // Indicates if the inequality is of type ≤ (true) or < (false) + // Constant value c in the inequality ax + by ≤ c + private int c; + + // Map containing the coefficients of the variables (e.g., a for ax, b for by) + public Map variableCoefficientsMap; + + public LinearInequality(Map variableCoefficientsMap, int constantTerm) { + this.variableCoefficientsMap = new HashMap<>(variableCoefficientsMap); + this.c = constantTerm; + } + + public boolean equals(LinearInequality otherInequality) { + if (this == otherInequality) return true; + return variableCoefficientsMap.equals(otherInequality.variableCoefficientsMap) + && c == otherInequality.c; + } + + public int getConstant() { + return c; + } + + @Override + public String toString() { + StringBuilder result = new StringBuilder(); + boolean isFirstTerm = true; + + for (Map.Entry entry : variableCoefficientsMap.entrySet()) { + int coefficientValue = entry.getValue(); + if (!isFirstTerm && coefficientValue > 0) result.append(" + "); // If it's not the first term AND the coefficient is positive + else if (!isFirstTerm) result.append(" - "); // If it's not the first term AND the coefficient is negative + else if (coefficientValue < 0) result.append("-"); // If it's the first term and it's negative, display only "-" + + // If the absolute value of the coefficient is not 1, explicitly append the coefficient before "*" + if (Math.abs(Math.abs(coefficientValue) - 1) > 0) { + result.append(Math.abs(coefficientValue)).append("*"); + } + + // Append the name of the variable (identifier) associated with the coefficient + result.append(entry.getKey().getName()); + // Mark that the first term has been processed + isFirstTerm = false; + } + + if (isLessOrEqualConstraint) + result.append(" <= "); + else + result.append(" < "); + result.append(c); + return result.toString(); + } + } + + public TwoVariablesInequalityDomain forgetIdentifier(Identifier varId) throws SemanticException { + return this; + } + + public Satisfiability satisfies(ValueExpression expr, ProgramPoint pp, SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } +} \ No newline at end of file diff --git a/src/test/java/it/unive/lisa/tutorial/IntervalSafeOveflowAndLinearInequalityCartesianProductTest.java b/src/test/java/it/unive/lisa/tutorial/IntervalSafeOveflowAndLinearInequalityCartesianProductTest.java new file mode 100644 index 0000000..e8ad72e --- /dev/null +++ b/src/test/java/it/unive/lisa/tutorial/IntervalSafeOveflowAndLinearInequalityCartesianProductTest.java @@ -0,0 +1,49 @@ +package it.unive.lisa.tutorial; + +import it.unive.lisa.AnalysisException; +import it.unive.lisa.DefaultConfiguration; +import it.unive.lisa.LiSA; +import it.unive.lisa.analysis.heap.pointbased.FieldSensitivePointBasedHeap; +import it.unive.lisa.conf.LiSAConfiguration; +import it.unive.lisa.conf.LiSAConfiguration.GraphType; +import it.unive.lisa.imp.IMPFrontend; +import it.unive.lisa.imp.ParsingException; +import it.unive.lisa.program.Program; +import org.junit.Test; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; + + +public class IntervalSafeOveflowAndLinearInequalityCartesianProductTest { + + @Test + public void testUpperBounds() throws ParsingException, AnalysisException { + // we parse the program to get the CFG representation of the code in it + Program program = IMPFrontend.processFile("inputs/ProduitCartesien.imp"); + + // we build a new configuration for the analysis + LiSAConfiguration conf = new DefaultConfiguration(); + + // we specify where we want files to be generated + conf.workdir = "outputs/ProduitCartesien"; + + // we specify the visual format of the analysis results + conf.analysisGraphs = GraphType.HTML; + + // we specify the analysis that we want to execute + var twoVariablesInequality = TwoVariablesInequalityDomain.TOP; + var extendedSigns = new ValueEnvironment<>(new IntervalSafeOverflowDomain()); + conf.abstractState = DefaultConfiguration.simpleState( + new FieldSensitivePointBasedHeap(), + new IntervalSafeOverflowTwoVariablesInequalityCartesianProduct( + twoVariablesInequality, + extendedSigns + ), + DefaultConfiguration.defaultTypeDomain()); + + // we instantiate LiSA with our configuration + LiSA lisa = new LiSA(conf); + + // finally, we tell LiSA to analyze the program + lisa.run(program); + } +} \ No newline at end of file diff --git a/src/test/java/it/unive/lisa/tutorial/IntervalleSafeOverflowTest.java b/src/test/java/it/unive/lisa/tutorial/IntervalleSafeOverflowTest.java new file mode 100644 index 0000000..888a46f --- /dev/null +++ b/src/test/java/it/unive/lisa/tutorial/IntervalleSafeOverflowTest.java @@ -0,0 +1,45 @@ +package it.unive.lisa.tutorial; + +import it.unive.lisa.AnalysisException; +import it.unive.lisa.DefaultConfiguration; +import it.unive.lisa.LiSA; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.conf.LiSAConfiguration; +import it.unive.lisa.conf.LiSAConfiguration.GraphType; +import it.unive.lisa.imp.IMPFrontend; +import it.unive.lisa.imp.ParsingException; +import it.unive.lisa.interprocedural.ReturnTopPolicy; +import it.unive.lisa.program.Program; +import org.junit.Test; + +public class IntervalleSafeOverflowTest { + + @Test + public void testInterval() throws ParsingException, AnalysisException { + // we parse the program to get the CFG representation of the code in it + Program program = IMPFrontend.processFile("inputs/IntervalleSafeOverflow.imp"); + + // we build a new configuration for the analysis + LiSAConfiguration conf = new DefaultConfiguration(); + + // we specify where we want files to be generated + conf.workdir = "outputs/IntervalSafeOverflowDomain"; + + // we specify the visual format of the analysis results + conf.analysisGraphs = GraphType.HTML; + + // we specify the analysis that we want to execute + conf.abstractState = DefaultConfiguration.simpleState( + DefaultConfiguration.defaultHeapDomain(), + new ValueEnvironment<>(new IntervalSafeOverflowDomain()), + DefaultConfiguration.defaultTypeDomain()); + + conf.openCallPolicy = ReturnTopPolicy.INSTANCE; + + // we instantiate LiSA with our configuration + LiSA lisa = new LiSA(conf); + + // finally, we tell LiSA to analyze the program + lisa.run(program); + } +} \ No newline at end of file diff --git a/src/test/java/it/unive/lisa/tutorial/TwoVariablesInequalityTest.java b/src/test/java/it/unive/lisa/tutorial/TwoVariablesInequalityTest.java new file mode 100644 index 0000000..8ab5dad --- /dev/null +++ b/src/test/java/it/unive/lisa/tutorial/TwoVariablesInequalityTest.java @@ -0,0 +1,43 @@ +package it.unive.lisa.tutorial; + +import it.unive.lisa.AnalysisException; +import it.unive.lisa.DefaultConfiguration; +import it.unive.lisa.LiSA; +import it.unive.lisa.analysis.heap.pointbased.FieldSensitivePointBasedHeap; +import it.unive.lisa.conf.LiSAConfiguration; +import it.unive.lisa.conf.LiSAConfiguration.GraphType; +import it.unive.lisa.imp.IMPFrontend; +import it.unive.lisa.imp.ParsingException; +import it.unive.lisa.program.Program; +import org.junit.Test; + +public class TwoVariablesInequalityTest { + + @Test + public void testUpperBounds() throws ParsingException, AnalysisException { + // we parse the program to get the CFG representation of the code in it + Program program = IMPFrontend.processFile("inputs/TwoVariablesInequality.imp"); + + // we build a new configuration for the analysis + LiSAConfiguration conf = new DefaultConfiguration(); + + // we specify where we want files to be generated + conf.workdir = "outputs/TwoVariablesInequality"; + + // we specify the visual format of the analysis results + conf.analysisGraphs = GraphType.HTML; + + // we specify the analysis that we want to execute + + conf.abstractState = DefaultConfiguration.simpleState( + new FieldSensitivePointBasedHeap(), + TwoVariablesInequalityDomain.TOP, + DefaultConfiguration.defaultTypeDomain()); + + // we instantiate LiSA with our configuration + LiSA lisa = new LiSA(conf); + + // finally, we tell LiSA to analyze the program + lisa.run(program); + } +} \ No newline at end of file