Bump JBSE

Bumping JBSE to latest version.

Signed-off-by: Alessandro Pellegrini <[email protected]>

data/jre/rt/META-INF/MANIFEST.MF

@@ -0,0 +1,120 @@
+Manifest-Version: 1.0
+Implementation-Vendor: Sun Microsystems, Inc.
+Implementation-Title: Java Runtime Environment
+Implementation-Version: 1.6.0_04
+Specification-Vendor: Sun Microsystems, Inc.
+Created-By: 1.6.0_04 (Sun Microsystems Inc.)
+Specification-Title: Java Platform API Specification
+Specification-Version: 1.6
+
+Name: javax/swing/JCheckBoxMenuItem.class
+Java-Bean: True
+
+Name: javax/swing/JDialog.class
+Java-Bean: True
+
+Name: javax/swing/JSlider.class
+Java-Bean: True
+
+Name: javax/swing/JTextField.class
+Java-Bean: True
+
+Name: javax/swing/JTextPane.class
+Java-Bean: True
+
+Name: javax/swing/JTextArea.class
+Java-Bean: True
+
+Name: javax/swing/JList.class
+Java-Bean: True
+
+Name: javax/swing/JFormattedTextField.class
+Java-Bean: True
+
+Name: javax/swing/JApplet.class
+Java-Bean: True
+
+Name: javax/swing/JSpinner.class
+Java-Bean: True
+
+Name: javax/swing/JLabel.class
+Java-Bean: True
+
+Name: javax/swing/JSplitPane.class
+Java-Bean: True
+
+Name: javax/swing/JSeparator.class
+Java-Bean: True
+
+Name: javax/swing/JComboBox.class
+Java-Bean: True
+
+Name: javax/swing/JMenuItem.class
+Java-Bean: True
+
+Name: javax/swing/JScrollBar.class
+Java-Bean: True
+
+Name: javax/swing/JCheckBox.class
+Java-Bean: True
+
+Name: javax/swing/JTabbedPane.class
+Java-Bean: True
+
+Name: javax/swing/JTable.class
+Java-Bean: True
+
+Name: javax/swing/JEditorPane.class
+Java-Bean: True
+
+Name: javax/swing/JProgressBar.class
+Java-Bean: True
+
+Name: javax/swing/JButton.class
+Java-Bean: True
+
+Name: javax/swing/JPopupMenu.class
+Java-Bean: True
+
+Name: javax/swing/JRadioButtonMenuItem.class
+Java-Bean: True
+
+Name: javax/swing/JMenuBar.class
+Java-Bean: True
+
+Name: javax/swing/JToggleButton.class
+Java-Bean: True
+
+Name: javax/swing/JWindow.class
+Java-Bean: True
+
+Name: javax/swing/JInternalFrame.class
+Java-Bean: True
+
+Name: javax/swing/JPanel.class
+Java-Bean: True
+
+Name: javax/swing/JToolBar.class
+Java-Bean: True
+
+Name: javax/swing/JFrame.class
+Java-Bean: True
+
+Name: javax/swing/JScrollPane.class
+Java-Bean: True
+
+Name: javax/swing/JTree.class
+Java-Bean: True
+
+Name: javax/swing/JMenu.class
+Java-Bean: True
+
+Name: javax/swing/JPasswordField.class
+Java-Bean: True
+
+Name: javax/swing/JRadioButton.class
+Java-Bean: True
+
+Name: javax/swing/JOptionPane.class
+Java-Bean: True
+

src/main/java/it/cnr/saks/hyperion/DecisionProcedureGuidance.java

@@ -209,23 +209,6 @@ protected final Outcome decide_XASTORE_Nonconcrete(Primitive inRange, SortedSet<
         return retVal;
     }
 
-    @Override
-    protected final Outcome resolve_XLOAD_GETX_Unresolved(State state, ReferenceSymbolic refToLoad, SortedSet<DecisionAlternative_XLOAD_GETX> result)
-    throws DecisionException, ClassFileNotFoundException, ClassFileIllFormedException, 
-    BadClassFileVersionException, RenameUnsupportedException, WrongClassNameException, 
-    IncompatibleClassFileException, ClassFileNotAccessibleException {
-        updateExpansionBackdoor(state, refToLoad);
-        final Outcome retVal = super.resolve_XLOAD_GETX_Unresolved(state, refToLoad, result);
-        if (this.guiding) {
-            final Iterator<DecisionAlternative_XLOAD_GETX> it = result.iterator();
-            while (it.hasNext()) {
-                final DecisionAlternative_XYLOAD_GETX_Unresolved dar = (DecisionAlternative_XYLOAD_GETX_Unresolved) it.next();
-                filter(state, refToLoad, dar, it);
-            }
-        }
-        return retVal;
-    }
-
     @Override
     protected final Outcome resolve_XALOAD_ResolvedNonconcrete(ArrayAccessInfo arrayAccessInfo, SortedSet<DecisionAlternative_XALOAD> result)
     throws DecisionException {
@@ -243,29 +226,6 @@ protected final Outcome resolve_XALOAD_ResolvedNonconcrete(ArrayAccessInfo array
         return retVal;
     }
 
-    @Override
-    protected final Outcome resolve_XALOAD_Unresolved(State state, ArrayAccessInfo arrayAccessInfo, SortedSet<DecisionAlternative_XALOAD> result)
-    throws DecisionException, ClassFileNotFoundException, ClassFileIllFormedException, 
-    BadClassFileVersionException, RenameUnsupportedException, WrongClassNameException, 
-    IncompatibleClassFileException, ClassFileNotAccessibleException {
-        final ReferenceSymbolic readReference = (ReferenceSymbolic) arrayAccessInfo.readValue;
-        updateExpansionBackdoor(state, readReference);
-        final Outcome retVal = super.resolve_XALOAD_Unresolved(state, arrayAccessInfo, result);
-        if (this.guiding) {
-            final Iterator<DecisionAlternative_XALOAD> it = result.iterator();
-            while (it.hasNext()) {
-                final DecisionAlternative_XALOAD_Unresolved dar = (DecisionAlternative_XALOAD_Unresolved) it.next();
-                final Primitive valueInConcreteState = this.jvm.eval_XALOAD(dar);
-                if (valueInConcreteState != null && valueInConcreteState.surelyFalse()) {
-                    it.remove();
-                } else {
-                    filter(state, readReference, dar, it);
-                }
-            }
-        }
-        return retVal;
-    }
-
     private void updateExpansionBackdoor(State state, ReferenceSymbolic refToLoad) throws GuidanceException {
         final String refType = className(refToLoad.getStaticType());
         final String objType = this.jvm.typeOfObject(refToLoad);

src/main/java/jbse/algo/Action_INIT.java

@@ -44,8 +44,8 @@ public void exec(State state, ExecutionContext ctx)
     throws DecisionException, ContradictionException, ThreadStackEmptyException, ClasspathException,
     CannotManageStateException, FailureException, InterruptException {
         try {
-            //pushes a frame for the root method (and possibly triggers)
             invokeRootMethod(state, ctx);
+            state.setStutters(false);
         } catch (HeapMemoryExhaustedException e) {
             throwNew(state, ctx.getCalculator(), OUT_OF_MEMORY_ERROR);
         }

src/main/java/jbse/algo/Action_START.java

@@ -95,7 +95,6 @@
 import jbse.jvm.exc.InitializationException;
 import jbse.mem.State;
 import jbse.mem.exc.ContradictionException;
-import jbse.mem.exc.FrozenStateException;
 import jbse.mem.exc.HeapMemoryExhaustedException;
 import jbse.mem.exc.InvalidProgramCounterException;
 import jbse.mem.exc.InvalidSlotException;
@@ -139,6 +138,7 @@ public void exec(ExecutionContext ctx)
             state = createStateStart(ctx);
             userProvidedStartState = false;
         }
+        state.setStutters(false);
 
         //adds the state to the state tree
         ctx.stateTree.addStateStart(state, userProvidedStartState);
@@ -350,7 +350,7 @@ private void initializeRootMethodClasses(State state, ExecutionContext ctx)
                     if (classFile == null) {
                         throw new ClasspathException("Root method invocation class " + className + " not found in the classpath.");
                     }
-                    ensureClassInitialized(state, classFile, ctx, this.doNotInitialize);
+                    ensureClassInitialized(state, ctx, this.doNotInitialize, classFile);
                 } catch (InterruptException e) {
                     //nothing to do: fall through
                 }
@@ -371,7 +371,7 @@ private void initializeClass(State state, String className, ExecutionContext ctx
             this.doNotInitialize.remove(className);
             final int classLoader = (JBSE_BASE.equals(className) ? CLASSLOADER_APP : CLASSLOADER_BOOT);
             final ClassFile classFile = state.getClassHierarchy().getClassFileClassArray(classLoader, className); 
-            ensureClassInitialized(state, classFile, ctx, this.doNotInitialize);
+            ensureClassInitialized(state, ctx, this.doNotInitialize, classFile);
         } catch (InterruptException e) {
             //nothing to do: fall through
         } catch (HeapMemoryExhaustedException | RenameUnsupportedException e) {
@@ -386,14 +386,18 @@ private void initializeClass(State state, String className, ExecutionContext ctx
 
     private void invokeGetSystemClassLoader(State state, ExecutionContext ctx) {
         try {
+        	final ClassFile cf_JAVA_OBJECT = state.getClassHierarchy().loadCreateClass(JAVA_OBJECT);
             final Snippet snippet = state.snippetFactoryNoWrap()
             .op_invokestatic(JAVA_CLASSLOADER_GETSYSTEMCLASSLOADER)
             .op_pop() //discards the return value
             .op_invokestatic(noclass_SETSTANDARDCLASSLOADERSREADY)
             .op_return()
             .mk();
-            state.pushSnippetFrameNoWrap(snippet, 0, CLASSLOADER_BOOT, "java/lang");
-        } catch (ThreadStackEmptyException | InvalidProgramCounterException | FrozenStateException e) {
+            state.pushSnippetFrameNoWrap(snippet, 0, cf_JAVA_OBJECT);
+        } catch (ThreadStackEmptyException | InvalidProgramCounterException |  
+        		InvalidInputException | ClassFileNotFoundException | ClassFileIllFormedException | 
+        		ClassFileNotAccessibleException | IncompatibleClassFileException | BadClassFileVersionException | 
+        		RenameUnsupportedException | WrongClassNameException e) {
             //this should not happen now
             failExecution(e);
         }

src/main/java/jbse/algo/Algo_BINMATHLOGICALOP.java

@@ -0,0 +1,65 @@
+package jbse.algo;
+
+import static jbse.bc.Offsets.MATH_LOGICAL_OP_OFFSET;
+
+import java.util.function.Supplier;
+
+import jbse.dec.DecisionProcedureAlgorithms;
+import jbse.tree.DecisionAlternative_NONE;
+
+/**
+ * {@link Algorithm} for all the binary mathematical
+ * and logical operator bytecodes.
+ * 
+ * @author Pietro Braione
+ */
+abstract class Algo_BINMATHLOGICALOP extends Algorithm<
+BytecodeData_0,
+DecisionAlternative_NONE,
+StrategyDecide<DecisionAlternative_NONE>, 
+StrategyRefine<DecisionAlternative_NONE>, 
+StrategyUpdate<DecisionAlternative_NONE>> {
+
+    @Override
+    protected final Supplier<Integer> numOperands() {
+        return () -> 2;
+    }
+
+    @Override
+    protected final Supplier<BytecodeData_0> bytecodeData() {
+        return BytecodeData_0::get;
+    }
+
+    @Override
+    protected final BytecodeCooker bytecodeCooker() {
+        return (state) -> { };
+    }
+
+    @Override
+    protected final Class<DecisionAlternative_NONE> classDecisionAlternative() {
+        return DecisionAlternative_NONE.class;
+    }
+
+    @Override
+    protected final StrategyDecide<DecisionAlternative_NONE> decider() {
+        return (state, result) -> { 
+            result.add(DecisionAlternative_NONE.instance());
+            return DecisionProcedureAlgorithms.Outcome.FF;
+        };
+    }
+
+    @Override
+    protected final StrategyRefine<DecisionAlternative_NONE> refiner() {
+        return (state, alt) -> { };
+    }
+
+    @Override
+    protected final Supplier<Boolean> isProgramCounterUpdateAnOffset() {
+        return () -> true;
+    }
+
+    @Override
+    protected final Supplier<Integer> programCounterUpdate() {
+        return () -> MATH_LOGICAL_OP_OFFSET;
+    }
+}

src/main/java/jbse/algo/Algo_GETSTATIC.java

@@ -49,7 +49,7 @@ protected Objekt source(State state)
     ContradictionException, FrozenStateException {
         //possibly initializes the class of the field
         try {
-            ensureClassInitialized(state, this.fieldClassResolved, this.ctx);
+            ensureClassInitialized(state, this.ctx, this.fieldClassResolved);
         } catch (HeapMemoryExhaustedException e) {
             throwNew(state, this.ctx.getCalculator(), OUT_OF_MEMORY_ERROR);
             exitFromAlgorithm();

src/main/java/jbse/algo/Algo_GETX.java

@@ -103,11 +103,6 @@ protected abstract void check(State state)
     protected abstract Objekt source(State state)
     throws ClasspathException, DecisionException, InterruptException, ContradictionException, FrozenStateException;
 
-    @Override
-    protected final Supplier<Boolean> isProgramCounterUpdateAnOffset() {
-        return () -> true;
-    }
-
     @Override
     protected final Supplier<Integer> programCounterUpdate() {
         return () -> GETX_PUTX_OFFSET;