Add missing swap instruction

regression/cbmc-java/swap1/Swap.java

@@ -0,0 +1,7 @@
+public class Swap {
+  public static void main(String[] args) {
+    int x = 5;
+    int result = x - 2;
+    assert result == -3;
+  }
+}

regression/cbmc-java/swap1/SwapDump.java

@@ -0,0 +1,108 @@
+import java.nio.file.Files;
+import java.nio.file.Paths;
+
+import org.objectweb.asm.*;
+public class SwapDump implements Opcodes {
+
+public static byte[] dump () throws Exception {
+
+ClassWriter cw = new ClassWriter(0);
+FieldVisitor fv;
+MethodVisitor mv;
+
+cw.visit(52, ACC_PUBLIC + ACC_SUPER, "Swap", null, "java/lang/Object", null);
+
+cw.visitSource("Swap.java", null);
+
+{
+fv = cw.visitField(ACC_FINAL + ACC_STATIC + ACC_SYNTHETIC, "$assertionsDisabled", "Z", null, null);
+fv.visitEnd();
+}
+{
+mv = cw.visitMethod(ACC_STATIC, "<clinit>", "()V", null, null);
+mv.visitCode();
+Label l0 = new Label();
+mv.visitLabel(l0);
+mv.visitLineNumber(1, l0);
+mv.visitLdcInsn(Type.getType("LSwap;"));
+mv.visitMethodInsn(INVOKEVIRTUAL, "java/lang/Class", "desiredAssertionStatus", "()Z", false);
+Label l1 = new Label();
+mv.visitJumpInsn(IFNE, l1);
+mv.visitInsn(ICONST_1);
+Label l2 = new Label();
+mv.visitJumpInsn(GOTO, l2);
+mv.visitLabel(l1);
+mv.visitFrame(Opcodes.F_SAME, 0, null, 0, null);
+mv.visitInsn(ICONST_0);
+mv.visitLabel(l2);
+mv.visitFrame(Opcodes.F_SAME1, 0, null, 1, new Object[] {Opcodes.INTEGER});
+mv.visitFieldInsn(PUTSTATIC, "Swap", "$assertionsDisabled", "Z");
+mv.visitInsn(RETURN);
+mv.visitMaxs(1, 0);
+mv.visitEnd();
+}
+{
+mv = cw.visitMethod(ACC_PUBLIC, "<init>", "()V", null, null);
+mv.visitCode();
+Label l0 = new Label();
+mv.visitLabel(l0);
+mv.visitLineNumber(1, l0);
+mv.visitVarInsn(ALOAD, 0);
+mv.visitMethodInsn(INVOKESPECIAL, "java/lang/Object", "<init>", "()V", false);
+mv.visitInsn(RETURN);
+Label l1 = new Label();
+mv.visitLabel(l1);
+mv.visitLocalVariable("this", "LSwap;", null, l0, l1, 0);
+mv.visitMaxs(1, 1);
+mv.visitEnd();
+}
+{
+mv = cw.visitMethod(ACC_PUBLIC + ACC_STATIC, "main", "([Ljava/lang/String;)V", null, null);
+mv.visitCode();
+Label l0 = new Label();
+mv.visitLabel(l0);
+mv.visitLineNumber(3, l0);
+mv.visitInsn(ICONST_5);
+mv.visitVarInsn(ISTORE, 1);
+Label l1 = new Label();
+mv.visitLabel(l1);
+mv.visitLineNumber(4, l1);
+mv.visitVarInsn(ILOAD, 1);
+mv.visitInsn(ICONST_2);
+mv.visitInsn(SWAP); // Manually added
+mv.visitInsn(ISUB);
+mv.visitVarInsn(ISTORE, 2);
+Label l2 = new Label();
+mv.visitLabel(l2);
+mv.visitLineNumber(5, l2);
+mv.visitFieldInsn(GETSTATIC, "Swap", "$assertionsDisabled", "Z");
+Label l3 = new Label();
+mv.visitJumpInsn(IFNE, l3);
+mv.visitVarInsn(ILOAD, 2);
+mv.visitIntInsn(BIPUSH, -3);
+mv.visitJumpInsn(IF_ICMPEQ, l3);
+mv.visitTypeInsn(NEW, "java/lang/AssertionError");
+mv.visitInsn(DUP);
+mv.visitMethodInsn(INVOKESPECIAL, "java/lang/AssertionError", "<init>", "()V", false);
+mv.visitInsn(ATHROW);
+mv.visitLabel(l3);
+mv.visitLineNumber(6, l3);
+mv.visitFrame(Opcodes.F_APPEND,2, new Object[] {Opcodes.INTEGER, Opcodes.INTEGER}, 0, null);
+mv.visitInsn(RETURN);
+Label l4 = new Label();
+mv.visitLabel(l4);
+mv.visitLocalVariable("args", "[Ljava/lang/String;", null, l0, l4, 0);
+mv.visitLocalVariable("x", "I", null, l1, l4, 1);
+mv.visitLocalVariable("result", "I", null, l2, l4, 2);
+mv.visitMaxs(2, 3);
+mv.visitEnd();
+}
+cw.visitEnd();
+
+return cw.toByteArray();
+}
+
+public static void main(String[] args) throws Exception {
+  Files.write(Paths.get("Swap.class"), dump());
+}
+}

regression/cbmc-java/swap1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Swap.class
+
+^EXIT=0
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/swap2/org/springframework/build/gradle/MergePlugin.groovy

@@ -0,0 +1,177 @@
+/*
+ * Copyright 2002-2015 the original author or authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+package org.springframework.build.gradle
+
+import org.gradle.api.*
+import org.gradle.api.artifacts.Configuration
+import org.gradle.api.artifacts.ProjectDependency;
+import org.gradle.api.artifacts.maven.Conf2ScopeMapping
+import org.gradle.api.plugins.MavenPlugin
+import org.gradle.plugins.ide.eclipse.EclipsePlugin
+import org.gradle.plugins.ide.idea.IdeaPlugin
+import org.gradle.api.invocation.*
+
+/**
+ * Gradle plugin that allows projects to merged together. Primarily developed to
+ * allow Spring to support multiple incompatible versions of third-party
+ * dependencies (for example Hibernate v3 and v4).
+ * <p>
+ * The 'merge' extension should be used to define how projects are merged, for example:
+ * <pre class="code">
+ * configure(subprojects) {
+ *     apply plugin: MergePlugin
+ * }
+ *
+ * project("myproject") {
+ * }
+ *
+ * project("myproject-extra") {
+ *     merge.into = project("myproject")
+ * }
+ * </pre>
+ * <p>
+ * This plugin adds two new configurations:
+ * <ul>
+ * <li>merging - Contains the projects being merged into this project<li>
+ * <li>runtimeMerge - Contains all dependencies that are merge projects. These are used
+ * to allow an IDE to reference merge projects.</li>
+ * <ul>
+ *
+ * @author Rob Winch
+ * @author Phillip Webb
+ */
+class MergePlugin implements Plugin<Project> {
+
+	private static boolean attachedProjectsEvaluated;
+
+	public void apply(Project project) {
+		project.plugins.apply(MavenPlugin)
+		project.plugins.apply(EclipsePlugin)
+		project.plugins.apply(IdeaPlugin)
+
+		MergeModel model = project.extensions.create("merge", MergeModel)
+		model.project = project
+		project.configurations.create("merging")
+		Configuration runtimeMerge = project.configurations.create("runtimeMerge")
+
+		// Ensure the IDE can reference merged projects
+		project.eclipse.classpath.plusConfigurations += [ runtimeMerge ]
+		project.idea.module.scopes.PROVIDED.plus += [ runtimeMerge ]
+
+		// Hook to perform the actual merge logic
+		project.afterEvaluate{
+			if (it.merge.into != null) {
+				setup(it)
+			}
+			setupIdeDependencies(it)
+		}
+
+		// Hook to build runtimeMerge dependencies
+		if (!attachedProjectsEvaluated) {
+			project.gradle.projectsEvaluated{
+				postProcessProjects(it)
+			}
+			attachedProjectsEvaluated  = true;
+		}
+	}
+
+	private void setup(Project project) {
+		project.merge.into.dependencies.add("merging", project)
+		project.dependencies.add("provided", project.merge.into.sourceSets.main.output)
+		project.dependencies.add("runtimeMerge", project.merge.into)
+		setupTaskDependencies(project)
+		setupMaven(project)
+	}
+
+	private void setupTaskDependencies(Project project) {
+		// invoking a task will invoke the task with the same name on 'into' project
+		["sourcesJar", "jar", "javadocJar", "javadoc", "install", "artifactoryPublish"].each {
+			def task = project.tasks.findByPath(it)
+			if (task) {
+				task.enabled = false
+				task.dependsOn(project.merge.into.tasks.findByPath(it))
+			}
+		}
+
+		// update 'into' project artifacts to contain the source artifact contents
+		project.merge.into.sourcesJar.from(project.sourcesJar.source)
+		project.merge.into.jar.from(project.sourceSets.main.output)
+		project.merge.into.javadoc {
+			source += project.javadoc.source
+			classpath += project.javadoc.classpath
+		}
+	}
+
+	private void setupIdeDependencies(Project project) {
+		project.configurations.each { c ->
+			c.dependencies.findAll( { it instanceof org.gradle.api.artifacts.ProjectDependency } ).each { d ->
+				d.dependencyProject.merge.from.each { from ->
+					project.dependencies.add("runtimeMerge", from)
+				}
+			}
+		}
+	}
+
+	private void setupMaven(Project project) {
+		project.configurations.each { configuration ->
+			Conf2ScopeMapping mapping = project.conf2ScopeMappings.getMapping([configuration])
+			if (mapping.scope) {
+				Configuration intoConfiguration = project.merge.into.configurations.create(
+					project.name + "-" + configuration.name)
+				configuration.excludeRules.each {
+					configuration.exclude([
+						(ExcludeRule.GROUP_KEY) : it.group,
+						(ExcludeRule.MODULE_KEY) : it.module])
+				}
+				configuration.dependencies.each {
+					def intoCompile = project.merge.into.configurations.getByName("compile")
+					// Protect against changing a compile scope dependency (SPR-10218)
+					if (!intoCompile.dependencies.contains(it)) {
+						intoConfiguration.dependencies.add(it)
+					}
+				}
+				def index = project.parent.childProjects.findIndexOf {p -> p.getValue() == project}
+				project.merge.into.install.repositories.mavenInstaller.pom.scopeMappings.addMapping(
+					mapping.priority + 100 + index, intoConfiguration, mapping.scope)
+			}
+		}
+	}
+
+	private postProcessProjects(Gradle gradle) {
+		gradle.allprojects(new Action<Project>() {
+			public void execute(Project project) {
+				project.configurations.getByName("runtime").allDependencies.withType(ProjectDependency).each{
+					Configuration dependsOnMergedFrom = it.dependencyProject.configurations.getByName("merging");
+					dependsOnMergedFrom.dependencies.each{ dep ->
+						project.dependencies.add("runtimeMerge", dep.dependencyProject)
+					}
+				}
+			}
+		});
+	}
+}
+
+class MergeModel {
+	Project project;
+	Project into;
+	List<Project> from = [];
+
+	public void setInto(Project into) {
+		this.into = into;
+		into.merge.from.add(project);
+	}
+}

regression/cbmc-java/swap2/test.desc

@@ -0,0 +1,8 @@
+CORE
+org/springframework/build/gradle/MergePlugin$1$_execute_closure1$_closure2.class
+--function "org.springframework.build.gradle.MergePlugin\$1\$_execute_closure1\$_closure2.\$getCallSiteArray:()[Lorg/codehaus/groovy/runtime/callsite/CallSite;"
+^EXIT=0
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2381,6 +2381,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
       call.add_source_location()=i_it->source_location;
       c=call;
     }
+    else if(statement=="swap")
+    {
+      assert(op.size()==2 && results.size()==2);
+      results[1]=op[0];
+      results[0]=op[1];
+    }
     else
     {
       c=codet(statement);