1 jSyX: Java Symbolic Execution Virtual Machine Eduardo Tarascón Quintas José Ángel García Fernández

2 1.Introducción 2.Creando una JVM 3.Ejecución simbólica 4.Cliente

3 1.Introducción 1.1 - ¿Qué es jSyX? 1.2 - Ejecución simbólica 1.3 – Posibles aplicaciones

4 jSyx es una máquina de ejecución simbólica de programas Java Además ofrece:  Ejecución normal de programas Java  Mostrar información sobre bytcode del archivo.class 1.1 – ¿Qué es jSyx?

5 1.Introducción 1.1 - ¿Qué es jSyX? 1.2 - Ejecución simbólica 1.3 – Posibles aplicaciones

6 1.2 – Ejecución simbólica La ejecución simbólica de programas consiste en una forma de ejecución donde se sustituyen los valores de entrada por símbolos formado por valores arbitrarios acotados. Esto dará como resultado múltiples caminos en los que los símbolos irán adquiriendo una serie de restricciones, dando lugar a un mapa completo de ejecución.

7 Ejemplo 1.2 – Ejecución simbólica Public abs(int x){ if (x>=0) return x else return –x; } -X se convertirá en un símbolo -Dos caminos de ejecución: -X >= 0 -X < 0 -Por la variación del flujo del programa sobre un símbolo entramos en una ejecución indeterminista

8 1.Introducción 1.1 - ¿Qué es jSyX? 1.2 - Ejecución simbólica 1.3 – Posibles aplicaciones

9 Uso: - Testing software - Verificación - Visualizadores - Depuradores Ejemplos: - PEX: genera tests para.NET - EXE: ejecución simbólica en C

10 Public abs(int x){ if (x>=0) return x else return –x; } Dos posibles casos: X >= 0 -> Valor concreto X = 0 X Valor concreto X = -1 1.3 – Posibles aplicaciones

11 1.Introducción 2.Creando una JVM 3.Ejecución simbólica 4.Cliente

12 2.Creando una JVM 2.1 - Máquina virtuales 2.2 - Introducción a una JVM 2.3 - Estructura 2.4 - Ejecución 2.5 - Archivos.class 2.6 - Implementación

13 Una máquina virtual es un contenedor de software que simula a un ordenador Se pueden englobar en 2 categorías:  Máquinas virtuales de sistema  Máquinas virtuales de proceso 2.1 – Máquinas virtuales

14 Máquina virtual de proceso Proporcionan un entorno de ejecución independiente del hardware y del sistema operativo subyacente. 2.1 – Máquinas virtuales ¡Rendimiento!

15 2.Creando una JVM 2.1 - Máquina virtuales 2.2 - Introducción a una JVM 2.3 - Estructura 2.4 - Ejecución 2.5 - Archivos.class 2.6 - Implementación

16 La JVM (Java Virtual Machine) es una máquina virtual de proceso que permite que cualquier programa Java se pueda ejecutar sobre cualquier plataforma Los programas en Java (.java) son traducidos a un código intermedio denominado bytecode.  Similar en formato a un código ensamblador.  Mas abstracto que un código máquina.  Permite disminuir la dependencia respecto del hardware específico. 2.2 – Introducción a una JVM “Write once, Run anywhere”

17 El bytecode se agrupa en archivos.class, que contienen la información de cada clase y las instrucciones. Estos archivos son cargados dinámicamente en un intérprete para su ejecución. El interprete permite la ejecución directa del bytecode o la compilación conocida como just- in-time (JIT) a código máquina nativo del sistema para mejorar el rendimiento. 2.2 – Introducción a una JVM

18 Esquema de trabajo de Java

19 2.Creando una JVM 2.1 - Máquina virtuales 2.2 - Introducción a una JVM 2.3 - Estructura 2.4 - Ejecución 2.5 - Archivos.class 2.6 - Implementación

20 2.3 – Estructura Podemos ver a la JVM como una máquina con tres partes:  ClassArea: información de clases y métodos.  Heap: información de objetos dinámicos.  Java stack: información de cada frame.

21 2.Creando una JVM 2.1 - Máquina virtuales 2.2 - Introducción a una JVM 2.3 - Estructura 2.4 - Ejecución 2.5 - Archivos.class 2.6 - Implementación

22 2.4 – Ejecución La JVM sigue el patrón de un intérprete basado en pila creando un frame por cada ejecución de método, cuando el método termina el control pasa al frame padre. La ejecución se hace a través de 212 instrucciones que se ocupan de distintas tareas, si existen para distintos tipos usan un prefijo (i para integer, d para double, etc).

23  Operaciones con la pila: poner elementos (bipush), quitarlos (pop), duplicarlos (dup), etc.  Aritméticas: sumas, restas, multiplicaciones de distintos tipos (iadd, fadd, dmul).  Carga y guardado: cargar (iload) o guardar elementos desde memoria local (istore).  Control de flujo: salto mediante comparación de valores (if_icmpeq), a subrutina, por excepciones (athrow).  Acceso a campos: para acceder a campos de clases (getfield, putfield, etc).  Invocación de métodos: ya sean estáticos (invokestatic), de interfaces (invokeinterface), etc.  Objetos: para reservar memoria de objetos (new) o arrays (newarray).  Conversión de tipos: cambio de un tipo (f2i) a otro o comprobación de tipos (checkcast). 2.4 – Ejecución

24 2.Creando una JVM 2.1 - Máquina virtuales 2.2 - Introducción a una JVM 2.3 - Estructura 2.4 - Ejecución 2.5 - Archivos.class 2.6 - Implementación

25 Como hemos mencionado los archivos fuente de java son compilados a un archivo.class (agrupados en bytes). Estos son los que la JVM usa para la ejecución, conteniendo las instrucciones bytecode además de la información de cada clase, almacenada en una estructura llamada Constant Pool. Dichas instrucciones no utilizan la información de ejecución de clases, interfaces, arrays, etc, sino que hacen referencia a la información simbólica de la Constant Pool, así si una instrucción necesita saber sobre qué clase está ejecutando una instrucción getstatic, hará referencia a la Constant Pool y obtendrá esta información. 2.5 – Archivos.class

26 Los archivos.class comienzan con una cabecera con un magic number (0xCAFEBABE) y el número de versión.

27 2.5 – Archivos.class A continuación la Constant Pool

28 2.5 – Archivos.class Después vienen los derechos de acceso de la clase codificados mediante una máscara de bits.

29 2.5 – Archivos.class A continuación las interfaces implementadas por la clase y una lista de los campos y métodos de la clase.

30 2.5 – Archivos.class La última parte se reserva para los atributos de clase como puede ser el nombre del archivo fuente que originó el.class.

31 2.Creando una JVM 2.1 - Máquina virtuales 2.2 - Introducción a una JVM 2.3 - Estructura 2.4 - Ejecución 2.5 - Archivos.class 2.6 - Implementación

32 2.6 – Implementación BCEL La librería BCEL (Byte Code Engineering Library) es una librería para analizar, manipular y crear archivos Java Class. En nuestro contexto es una ayuda para parsear los archivos.class y obtener toda la información que necesitamos para la ejecución del bytecode en nuestra máquina virtual de Java jSyX. Hacemos uso de dos de los paquetes principales de BCEL.  org.apache.bcel.classfile: nos permite acceder a la información guardada en.class sin preocuparnos de lecturas de bajo nivel, aunque sin ningún tipo de modificación.  org.apache.bcel.generic: permite modificaciones.

33 2.6 – Implementación Paquetes Clases de prueba para ejecución

34 2.6 – Implementación Paquetes Clases para generación del archivo de log

35 2.6 – Implementación Paquetes En paquete principal (JVM.java, Heap.java, ClassArea.java,etc.)  En subpaquete test las relacionadas con la ejecución.  En subpaquete tipos la estructura de tipos.

36 2.6 – Implementación Clases La clase JVM contiene la máquina virtual en sí, contamos con las 3 zonas de memoria mencionadas, el StackFrame, el Heap y el ClassArea. El Heap lo hemos diseñado mediante un array de JValue y un puntero con la siguiente posición libre del array además disponemos de métodos para crear los distintos elementos dinámicos. El ClassArea que mantiene la información de clases se ha diseñado mediante un HashTable con clave el nombre de clase.

37 2.6 – Implementación Diagrama Estructura básica de clases

38 2.6 – Implementación Tipos de ejecución Como hemos mencionado tenemos 2 tipos de ejecución básica no simbólica:  OPCODE: leyendo directamente del bytecode, usando la clase Constants de BCEL para detectar la instrucción y ejecutar.  IHPC: haciendo uso del InstructionHandle se facilita en parte el trabajo de ejecución debido a que dicha clase nos da información de cada instrucción. Además se permite la ejecución de métodos nativos mediante la clase Natives. Ésta se realiza comprobando en la máquina virtual si el método está marcado con el flag NATIVE, si es así se obtiene su signature y se pasa a comprobar usando la clase Natives si se dispone de una implementación del mismo para su ejecución.

39 2.6 – Implementación Tipos En cuanto a tipos se han incluido los que maneja la máquina virtual además para facilitar el trabajo se han creado algunos elementos extra para el trabajo con arrays y objetos. La clase base es JValue, abstracta de la que todas los demás extienden que contiene un elemento Type de BCEL.

40 1.Introducción 2.Creando una JVM 3. Ejecución simbólica 4.Cliente

41 3.Ejecución Simbólica 1.1 – Ampliación Ejecución simbólica 1.2 – Programación con restricciones 1.3 – choco 1.4 – Algoritmo principal 1.5 – Ejemplo

42 Suministra símbolos en vez de entradas Símbolos están representados por restricciones Extensión de la ejecución concreta Ramas independientes Árboles con ramas infinitas 3.1 – Ampliación Ejecución Simbólica

43 3.Ejecución Simbólica 1.1 – Ampliación Ejecución simbólica 1.2 – Programación con restricciones 1.3 – choco 1.4 – Algoritmo principal 1.5 – Ejemplo

44 3.2 – Programación con restricciones La programación con restricciones es una aproximación alternativa a la programación en donde el proceso es limitado a la generación de unos requisitos(constraints) y una solución a dicho requisitos en términos generales o en un dominio específico. Carácterísticas: - Modelo(model): representación del problema por medio de constraints. - Resolutor(solver): resolución de dicho modelo.

45 3.Ejecución Simbólica 1.1 – Ampliación Ejecución simbólica 1.2 – Programación con restricciones 1.3 – choco 1.4 – Algoritmo principal 1.5 – Ejemplo

46 3.3 – choco Choco es una librería java para la programación con restricciones

47 3.Ejecución Simbólica 1.1 – Ampliación Ejecución simbólica 1.2 – Programación con restricciones 1.3 – choco 1.4 – Algoritmo principal 1.5 – Ejemplo

48 private void run_bt(int nivel, int últimaConstraint, bool últimaDecision){ while (esTopFrame?() && topFrameError?() && nivel < límite) { if (esNativo? ()) jecutarNativo(); else { ih = conseguirSiguienteInstruccion(); if (nuevaRama()){ if (ultimaDecisionTomada()){ //Rama Contraria ejecutarInstruccion(ih,false); últimaDecision != ultimaDecisión; } else { copia(); últimaConstraint = marcarUltimaConstraint(); ejecutarInstruccion(ih,false); if (!esHoja?()) run_bt(nivel++, últimaConstraint, últimaDecision); if (!esLimite()){ resetSolver(); eliminarConstraintsAcumuladas(); } //Restablecer estado lastDecission = !lastDecission; topFrame = parentFrame; heap = parentHeap; }else ejecutarIH(ih, false); } if (esHoja?()){ solucionarSolver(); guardarSolución(); } else { imprimirErrorMaxNivel(); } 3.4 – Algoritmo principal

49 3.Ejecución Simbólica 1.1 – Ampliación Ejecución simbólica 1.2 – Programación con restricciones 1.3 – choco 1.4 – Algoritmo principal 1.5 – Ejemplo

50 3.5 – Ejemplo public static int intExp(int a, int n) throws Throwable { if (n < 0) // Exponent must be non-negative throw new Throwable(); else if ((a == 0) && (n == 0)) // 0 to 0 is undefined throw new Throwable(); else { int out = 1; for (; n > 0; n--) out = out * a; return out; } Código Java

51 3.5 – Ejemplo    

52 Árbol de ejecución 3.5 – Ejemplo −

53 1.Introducción 2.Creando una JVM 3.Ejecución simbólica 4.Cliente

54 4.1 – Información General 4.2 – Commons CLI 4.3 – Implementación 4.4 - Ejemplos de uso

55 El programa cliente permite tanto la ejecución simbólica como la no simbólica permitiendo el uso de parámetros para acceder a distintas funcionalidades. 4.1 – Información General

56 4.Cliente 4.1 – Información General 4.2 – Commons CLI 4.3 – Implementación 4.4 - Ejemplos de uso

57 Proporciona una API para parsear opciones de línea de comandos pasados a programas. Además permite generar mensajes de ayuda automáticamente a partir de las opciones disponibles. Hay 3 etapas a la hora de procesar los parámetros de línea de comandos:  Definición  Parseo  Interrogatorio 4.2 – Commons CLI

58 4.Cliente 4.1 – Información General 4.2 – Commons CLI 4.3 – Implementación 4.4 - Ejemplos de uso

59 La clase Exec es el punto de partida para la ejecución. 4.3 – Implementación Estructura básica

60 4.Cliente 4.1 – Información General 4.2 – Commons CLI 4.3 – Implementación 4.4 - Ejemplos de uso

61 4.4 – Ejemplos de uso Ejemplo 1 public class A { private int campo1; public static int campo2; public A(int a, int b){ campo1 = a; campo2 = b; } public int getCampo1(){ return campo1; } public void setCampo1(int a){ campo1 = a; } public void operacion(){ for (int i = 0; i < 10;i++) { if (campo1 < 2) campo2++; } public static native void nativo1(); public static native void nativo2(); }

62 4.4 – Ejemplos de uso Ejecución no simbólica obteniendo información de clase

63 4.4 – Ejemplos de uso Ejecución no simbólica obteniendo información de clase Podemos ver la Constant Pool y también una descripción de los métodos de la clase

64 4.4 – Ejemplos de uso public static int abs(int x) { if (x >= 0) return x; else return -x; } 0: iload_0 1: iflt #6 4: iload_0 5: ireturn 6: iload_0 7: ineg 8: ireturn Ejemplo 2

65 4.4 – Ejemplos de uso Ejecución simbólica de método de clase