Skip to content

Commit

Permalink
Merge pull request #948 from GaloisInc/jvm-setup-error
Browse files Browse the repository at this point in the history 
Error checking for JVMSetup commands
  • Loading branch information
brianhuffman authored Dec 4, 2020
2 parents 6f73c07 + 8cb78f5 commit e8bbe57
Show file tree
Hide file tree
Showing 7 changed files with 293 additions and 135 deletions.
46 changes: 24 additions & 22 deletions intTests/test_jvm_setup_errors/test.saw
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ check_fails test "get"
};

print "jvm_field_is with previous jvm_field_is on same field";
KNOWN_FALSE_POSITIVE test "get"
check_fails test "get"
do {
this <- jvm_alloc_object "Test";
val <- jvm_fresh_var "val" java_long;
Expand Down Expand Up @@ -198,7 +198,7 @@ check_fails test "lookup"
};

print "jvm_elem_is with index out of bounds";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
arr <- jvm_alloc_array 8 java_long;
let idx = {{ 12 : [32] }};
Expand Down Expand Up @@ -245,7 +245,7 @@ crucible_jvm_verify test "lookup" [] false
} z3;

print "jvm_array_is with non-monomorphic type";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
arr <- jvm_alloc_array 8 java_long;
let xs = {{ zero }};
Expand All @@ -256,7 +256,7 @@ KNOWN_FALSE_POSITIVE test "lookup"
};

print "jvm_array_is with non-array type";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
arr <- jvm_alloc_array 8 java_long;
let xs = {{ (True, False) }};
Expand All @@ -267,7 +267,7 @@ KNOWN_FALSE_POSITIVE test "lookup"
};

print "jvm_array_is with wrong array length";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
arr <- jvm_alloc_array 8 java_long;
xs <- jvm_fresh_var "xs" (java_array 4 java_long);
Expand All @@ -278,7 +278,7 @@ KNOWN_FALSE_POSITIVE test "lookup"
};

print "jvm_array_is with non-jvm element type";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
arr <- jvm_alloc_array 8 java_long;
let xs = {{ zero : [8]Integer }};
Expand All @@ -289,7 +289,7 @@ KNOWN_FALSE_POSITIVE test "lookup"
};

print "jvm_array_is with wrong array element type";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
arr <- jvm_alloc_array 8 java_long;
xs <- jvm_fresh_var "xs" (java_array 8 java_int);
Expand All @@ -300,7 +300,7 @@ KNOWN_FALSE_POSITIVE test "lookup"
};

print "jvm_array_is with object reference";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
arr <- jvm_alloc_object "Test";
xs <- jvm_fresh_var "xs" (java_array 8 java_long);
Expand All @@ -311,7 +311,7 @@ KNOWN_FALSE_POSITIVE test "lookup"
};

print "jvm_array_is with null reference";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
let arr = jvm_null;
xs <- jvm_fresh_var "xs" (java_array 8 java_long);
Expand All @@ -322,7 +322,7 @@ KNOWN_FALSE_POSITIVE test "lookup"
};

print "jvm_array_is with non-reference";
KNOWN_FALSE_POSITIVE test "lookup"
check_fails test "lookup"
do {
let arr = jvm_term {{ True }};
xs <- jvm_fresh_var "xs" (java_array 8 java_long);
Expand Down Expand Up @@ -366,7 +366,7 @@ crucible_jvm_verify test "set" [] false
} z3;

print "jvm_execute_func with non-monomorphic types";
KNOWN_FALSE_POSITIVE test "set"
check_fails test "set"
do {
this <- jvm_alloc_object "Test";
x <- jvm_fresh_var "x" java_long;
Expand All @@ -375,7 +375,7 @@ KNOWN_FALSE_POSITIVE test "set"
};

print "jvm_execute_func with non-jvm types";
KNOWN_FALSE_POSITIVE test "set"
check_fails test "set"
do {
this <- jvm_alloc_object "Test";
x <- jvm_fresh_var "x" java_long;
Expand All @@ -384,7 +384,7 @@ KNOWN_FALSE_POSITIVE test "set"
};

print "jvm_execute_func with wrong types";
KNOWN_FALSE_POSITIVE test "set"
check_fails test "set"
do {
this <- jvm_alloc_object "Test";
x <- jvm_fresh_var "x" java_long;
Expand All @@ -393,7 +393,7 @@ KNOWN_FALSE_POSITIVE test "set"
};

print "jvm_execute_func with reference type when base type was expected";
KNOWN_FALSE_POSITIVE test "set"
check_fails test "set"
do {
this <- jvm_alloc_object "Test";
x <- jvm_fresh_var "x" java_long;
Expand All @@ -402,7 +402,7 @@ KNOWN_FALSE_POSITIVE test "set"
};

print "jvm_execute_func with base type when reference type was expected";
KNOWN_FALSE_POSITIVE test "set"
check_fails test "set"
do {
this <- jvm_alloc_object "Test";
x <- jvm_fresh_var "x" java_long;
Expand All @@ -411,7 +411,7 @@ KNOWN_FALSE_POSITIVE test "set"
};

print "jvm_execute_func with too few arguments";
KNOWN_FALSE_POSITIVE test "set"
check_fails test "set"
do {
this <- jvm_alloc_object "Test";
x <- jvm_fresh_var "x" java_long;
Expand All @@ -420,7 +420,7 @@ KNOWN_FALSE_POSITIVE test "set"
};

print "jvm_execute_func with too many arguments";
KNOWN_FALSE_POSITIVE test "set"
check_fails test "set"
do {
this <- jvm_alloc_object "Test";
x <- jvm_fresh_var "x" java_long;
Expand All @@ -429,7 +429,7 @@ KNOWN_FALSE_POSITIVE test "set"
};

print "jvm_return with non-monomorphic type";
KNOWN_FALSE_POSITIVE test "get"
check_fails test "get"
do {
this <- jvm_alloc_object "Test";
val <- jvm_fresh_var "val" java_long;
Expand All @@ -439,7 +439,7 @@ KNOWN_FALSE_POSITIVE test "get"
};

print "jvm_return with non-jvm type";
KNOWN_FALSE_POSITIVE test "get"
check_fails test "get"
do {
this <- jvm_alloc_object "Test";
val <- jvm_fresh_var "val" java_long;
Expand All @@ -449,7 +449,7 @@ KNOWN_FALSE_POSITIVE test "get"
};

print "jvm_return with wrong base type";
KNOWN_FALSE_POSITIVE test "get"
check_fails test "get"
do {
this <- jvm_alloc_object "Test";
val <- jvm_fresh_var "val" java_long;
Expand All @@ -459,7 +459,7 @@ KNOWN_FALSE_POSITIVE test "get"
};

print "jvm_return with reference type when base type was expected";
KNOWN_FALSE_POSITIVE test "get"
check_fails test "get"
do {
this <- jvm_alloc_object "Test";
val <- jvm_fresh_var "val" java_long;
Expand All @@ -478,11 +478,13 @@ KNOWN_FALSE_POSITIVE test "get"
};

print "jvm_return when none was expected";
KNOWN_FALSE_POSITIVE test "set"
check_fails test "set"
do {
this <- jvm_alloc_object "Test";
x <- jvm_fresh_var "x" java_long;
jvm_execute_func [this, jvm_term x];
jvm_field_is this "val" (jvm_term x);
jvm_return (jvm_term x);
};

print "DONE!";
5 changes: 4 additions & 1 deletion src/SAWScript/Crucible/Common/MethodSpec.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext)
ppSetupValue :: SetupValue ext -> PP.Doc ann
ppSetupValue setupval = case setupval of
SetupTerm tm -> ppTypedTerm tm
SetupVar i -> PP.pretty ("@" ++ show i)
SetupVar i -> ppAllocIndex i
SetupNull _ -> PP.pretty "NULL"
SetupStruct _ packed vs
| packed -> PP.angles (PP.braces (commaList (map ppSetupValue vs)))
Expand All @@ -141,6 +141,9 @@ ppSetupValue setupval = case setupval of
commaList [] = PP.emptyDoc
commaList (x:xs) = x PP.<> PP.hcat (map (\y -> PP.comma PP.<+> y) xs)

ppAllocIndex :: AllocIndex -> PP.Doc ann
ppAllocIndex i = PP.pretty '@' <> PP.viaShow i

ppTypedTerm :: TypedTerm -> PP.Doc ann
ppTypedTerm (TypedTerm tp tm) =
PP.unAnnotate (ppTerm defaultPPOpts tm)
Expand Down
Loading

0 comments on commit e8bbe57

Please sign in to comment.