-
Notifications
You must be signed in to change notification settings - Fork 20
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- added encoder api - added implementations for 'Engine' methods
- Loading branch information
1 parent
6680dc4
commit c81dc1f
Showing
3 changed files
with
46 additions
and
38 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,121 +1,115 @@ | ||
package org.usvm.api; | ||
|
||
import org.usvm.api.internal.SymbolicIdentityMapImpl; | ||
import org.usvm.api.internal.SymbolicListImpl; | ||
import org.usvm.api.internal.SymbolicMapImpl; | ||
|
||
import java.lang.reflect.Array; | ||
|
||
public class Engine { | ||
|
||
public static void assume(boolean expr) { | ||
engineApiStubError(); | ||
assert expr; | ||
} | ||
|
||
@SuppressWarnings("unused") | ||
public static <T> T makeSymbolic(Class<T> clazz) { | ||
engineApiStubError(); | ||
return null; | ||
} | ||
|
||
@SuppressWarnings("unused") | ||
public static <T> T makeNullableSymbolic(Class<T> clazz) { | ||
return null; | ||
} | ||
|
||
public static boolean makeSymbolicBoolean() { | ||
engineApiStubError(); | ||
return false; | ||
} | ||
|
||
public static byte makeSymbolicByte() { | ||
engineApiStubError(); | ||
return 0; | ||
} | ||
|
||
public static char makeSymbolicChar() { | ||
engineApiStubError(); | ||
return 0; | ||
} | ||
|
||
public static short makeSymbolicShort() { | ||
engineApiStubError(); | ||
return 0; | ||
} | ||
|
||
public static int makeSymbolicInt() { | ||
engineApiStubError(); | ||
return 0; | ||
} | ||
|
||
public static long makeSymbolicLong() { | ||
engineApiStubError(); | ||
return 0; | ||
} | ||
|
||
public static float makeSymbolicFloat() { | ||
engineApiStubError(); | ||
return 0; | ||
} | ||
|
||
public static double makeSymbolicDouble() { | ||
engineApiStubError(); | ||
return 0; | ||
} | ||
|
||
@SuppressWarnings("unchecked") | ||
public static <T> T[] makeSymbolicArray(Class<T> clazz, int size) { | ||
engineApiStubError(); | ||
return null; | ||
assert clazz.isArray(); | ||
|
||
return (T[]) Array.newInstance(clazz, size); | ||
} | ||
|
||
public static boolean[] makeSymbolicBooleanArray(int size) { | ||
engineApiStubError(); | ||
return null; | ||
return new boolean[size]; | ||
} | ||
|
||
public static byte[] makeSymbolicByteArray(int size) { | ||
engineApiStubError(); | ||
return null; | ||
return new byte[size]; | ||
} | ||
|
||
public static char[] makeSymbolicCharArray(int size) { | ||
engineApiStubError(); | ||
return null; | ||
return new char[size]; | ||
} | ||
|
||
public static short[] makeSymbolicShortArray(int size) { | ||
engineApiStubError(); | ||
return null; | ||
return new short[size]; | ||
} | ||
|
||
public static int[] makeSymbolicIntArray(int size) { | ||
engineApiStubError(); | ||
return null; | ||
return new int[size]; | ||
} | ||
|
||
public static long[] makeSymbolicLongArray(int size) { | ||
engineApiStubError(); | ||
return null; | ||
return new long[size]; | ||
} | ||
|
||
public static float[] makeSymbolicFloatArray(int size) { | ||
engineApiStubError(); | ||
return null; | ||
return new float[size]; | ||
} | ||
|
||
public static double[] makeSymbolicDoubleArray(int size) { | ||
engineApiStubError(); | ||
return null; | ||
return new double[size]; | ||
} | ||
|
||
public static <T> SymbolicList<T> makeSymbolicList() { | ||
engineApiStubError(); | ||
return null; | ||
return new SymbolicListImpl<>(); | ||
} | ||
|
||
public static <K, V> SymbolicMap<K, V> makeSymbolicMap() { | ||
engineApiStubError(); | ||
return null; | ||
return new SymbolicMapImpl<>(); | ||
} | ||
|
||
public static <K, V> SymbolicIdentityMap<K, V> makeSymbolicIdentityMap() { | ||
engineApiStubError(); | ||
return null; | ||
return new SymbolicIdentityMapImpl<>(); | ||
} | ||
|
||
public static boolean typeEquals(Object a, Object b) { | ||
engineApiStubError(); | ||
return false; | ||
return a.getClass() == b.getClass(); | ||
} | ||
|
||
private static void engineApiStubError() { | ||
throw new IllegalStateException("Engine API method must not be invoked"); | ||
public static boolean typeIs(Object a, Class<?> type) { | ||
return a.getClass() == type; | ||
} | ||
} |
9 changes: 9 additions & 0 deletions
9
usvm-jvm/src/usvm-api/java/org/usvm/api/encoder/EncoderFor.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
package org.usvm.api.encoder; | ||
|
||
import java.lang.annotation.ElementType; | ||
import java.lang.annotation.Target; | ||
|
||
@Target({ElementType.TYPE}) | ||
public @interface EncoderFor { | ||
Class<?> value(); | ||
} |
5 changes: 5 additions & 0 deletions
5
usvm-jvm/src/usvm-api/java/org/usvm/api/encoder/ObjectEncoder.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
package org.usvm.api.encoder; | ||
|
||
public interface ObjectEncoder { | ||
Object encode(Object object); | ||
} |