Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
S
seer
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Nils Fitinghoff
seer
Commits
b2a7df97
Commit
b2a7df97
authored
Feb 20, 2018
by
nilfit
Browse files
Options
Downloads
Patches
Plain Diff
change functions to enable overflow checks for symbolic arithmetic
implemented check for unsigned ints
parent
8f234780
No related branches found
No related tags found
No related merge requests found
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/operator.rs
+43
-21
43 additions, 21 deletions
src/operator.rs
with
43 additions
and
21 deletions
src/operator.rs
+
43
−
21
View file @
b2a7df97
...
...
@@ -25,7 +25,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
op
:
mir
::
BinOp
,
left
:
&
mir
::
Operand
<
'tcx
>
,
right
:
&
mir
::
Operand
<
'tcx
>
,
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
boo
l
)
>
{
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
PrimVa
l
)
>
{
let
left_ty
=
self
.operand_ty
(
left
);
let
right_ty
=
self
.operand_ty
(
right
);
let
left_val
=
self
.eval_operand_to_primval
(
left
)
?
;
...
...
@@ -44,7 +44,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
dest_ty
:
Ty
<
'tcx
>
,
)
->
EvalResult
<
'tcx
>
{
let
(
val
,
overflowed
)
=
self
.binop_with_overflow
(
op
,
left
,
right
)
?
;
let
val
=
Value
::
ByValPair
(
val
,
PrimVal
::
from_bool
(
overflowed
)
)
;
let
val
=
Value
::
ByValPair
(
val
,
overflowed
);
self
.write_value
(
ValTy
{
value
:
val
,
ty
:
dest_ty
},
dest
)
}
...
...
@@ -60,7 +60,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
)
->
EvalResult
<
'tcx
,
bool
>
{
let
(
val
,
overflowed
)
=
self
.binop_with_overflow
(
op
,
left
,
right
)
?
;
self
.write_primval
(
dest
,
val
,
dest_ty
)
?
;
Ok
(
overflowed
)
Ok
(
overflowed
.to_bool
()
?
)
}
}
...
...
@@ -68,7 +68,7 @@ macro_rules! overflow {
(
$op:ident
,
$l:expr
,
$r:expr
)
=>
({
let
(
val
,
overflowed
)
=
$l
.
$op
(
$r
);
let
primval
=
PrimVal
::
Bytes
(
val
as
u128
);
Ok
((
primval
,
overflowed
))
Ok
((
primval
,
PrimVal
::
from_bool
(
overflowed
))
)
})
}
...
...
@@ -122,7 +122,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
left_ty
:
Ty
<
'tcx
>
,
right
:
PrimVal
,
right_ty
:
Ty
<
'tcx
>
,
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
boo
l
)
>
{
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
PrimVa
l
)
>
{
use
rustc
::
mir
::
BinOp
::
*
;
use
value
::
PrimValKind
::
*
;
...
...
@@ -155,7 +155,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
Offset
if
left_kind
==
Ptr
&&
right_kind
==
usize
=>
{
let
pointee_ty
=
left_ty
.builtin_deref
(
true
)
.expect
(
"Offset called on non-ptr type"
)
.ty
;
let
ptr
=
self
.pointer_offset
(
left
,
pointee_ty
,
right
.to_bytes
()
?
as
i64
)
?
;
return
Ok
((
ptr
,
false
));
return
Ok
((
ptr
,
PrimVal
::
from_bool
(
false
))
)
;
},
// These work on anything
Eq
if
left_kind
==
right_kind
=>
{
...
...
@@ -165,7 +165,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
(
PrimVal
::
Undef
,
_
)
|
(
_
,
PrimVal
::
Undef
)
=>
return
Err
(
EvalError
::
ReadUndefBytes
),
_
=>
false
,
};
return
Ok
((
PrimVal
::
from_bool
(
result
),
false
));
return
Ok
((
PrimVal
::
from_bool
(
result
),
PrimVal
::
from_bool
(
false
))
)
;
}
Ne
if
left_kind
==
right_kind
=>
{
let
result
=
match
(
left
,
right
)
{
...
...
@@ -174,7 +174,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
(
PrimVal
::
Undef
,
_
)
|
(
_
,
PrimVal
::
Undef
)
=>
return
Err
(
EvalError
::
ReadUndefBytes
),
_
=>
true
,
};
return
Ok
((
PrimVal
::
from_bool
(
result
),
false
));
return
Ok
((
PrimVal
::
from_bool
(
result
),
PrimVal
::
from_bool
(
false
))
)
;
}
// These need both pointers to be in the same allocation
Lt
|
Le
|
Gt
|
Ge
|
Sub
...
...
@@ -200,7 +200,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
}
_
=>
bug!
(
"We already established it has to be one of these operators."
),
};
return
Ok
((
PrimVal
::
from_bool
(
res
),
false
));
return
Ok
((
PrimVal
::
from_bool
(
res
),
PrimVal
::
from_bool
(
false
))
)
;
}
else
{
// Both are pointers, but from different allocations.
return
Err
(
EvalError
::
InvalidPointerMath
);
...
...
@@ -297,7 +297,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
}
};
Ok
((
val
,
false
))
Ok
((
val
,
PrimVal
::
from_bool
(
false
))
)
}
fn
ptr_int_arithmetic
(
...
...
@@ -306,11 +306,11 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
left
:
MemoryPointer
,
right
:
i128
,
signed
:
bool
,
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
boo
l
)
>
{
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
PrimVa
l
)
>
{
use
rustc
::
mir
::
BinOp
::
*
;
fn
map_to_primval
((
res
,
over
)
:
(
MemoryPointer
,
bool
))
->
(
PrimVal
,
boo
l
)
{
(
PrimVal
::
Ptr
(
res
),
over
)
fn
map_to_primval
((
res
,
over
)
:
(
MemoryPointer
,
bool
))
->
(
PrimVal
,
PrimVa
l
)
{
(
PrimVal
::
Ptr
(
res
),
PrimVal
::
from_bool
(
over
)
)
}
let
left_offset
=
match
left
.offset
{
...
...
@@ -332,10 +332,10 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
let
right
=
right
as
u64
;
if
right
&
base_mask
==
base_mask
{
// Case 1: The base address bits are all preserved, i.e., right is all-1 there
(
PrimVal
::
Ptr
(
MemoryPointer
::
new
(
left
.alloc_id
,
left_offset
&
right
)),
false
)
(
PrimVal
::
Ptr
(
MemoryPointer
::
new
(
left
.alloc_id
,
left_offset
&
right
)),
PrimVal
::
from_bool
(
false
)
)
}
else
if
right
&
base_mask
==
0
{
// Case 2: The base address bits are all taken away, i.e., right is all-0 there
(
PrimVal
::
from_u128
((
left_offset
&
right
)
as
u128
),
false
)
(
PrimVal
::
from_u128
((
left_offset
&
right
)
as
u128
),
PrimVal
::
from_bool
(
false
)
)
}
else
{
return
Err
(
EvalError
::
ReadPointerAsBytes
);
}
...
...
@@ -355,7 +355,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
left_kind
:
PrimValKind
,
right
:
PrimVal
,
mut
right_kind
:
PrimValKind
,
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
boo
l
)
>
{
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
PrimVa
l
)
>
{
// These ops can have an RHS with a different numeric type.
if
bin_op
==
mir
::
BinOp
::
Shl
||
bin_op
==
mir
::
BinOp
::
Shr
{
...
...
@@ -368,7 +368,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
for
idx
in
num_bytes
..
8
{
buffer
[
idx
]
=
abytes
[
idx
-
num_bytes
];
}
return
Ok
((
PrimVal
::
Abstract
(
buffer
),
false
));
return
Ok
((
PrimVal
::
Abstract
(
buffer
),
PrimVal
::
from_bool
(
false
))
)
;
}
mir
::
BinOp
::
Shr
=>
{
if
!
left_kind
.is_signed_int
()
{
...
...
@@ -376,7 +376,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
for
idx
in
num_bytes
..
8
{
buffer
[
idx
-
num_bytes
]
=
abytes
[
idx
];
}
return
Ok
((
PrimVal
::
Abstract
(
buffer
),
false
));
return
Ok
((
PrimVal
::
Abstract
(
buffer
),
PrimVal
::
from_bool
(
false
))
)
;
}
}
_
=>
unimplemented!
(),
...
...
@@ -407,7 +407,29 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
let
msg
=
format!
(
"unimplemented binary op: {:?}, {:?}, {:?}"
,
left
,
right
,
bin_op
);
return
Err
(
EvalError
::
Unimplemented
(
msg
));
}
Ok
((
self
.memory.constraints
.add_binop_constraint
(
bin_op
,
left
,
right
,
left_kind
),
false
))
use
value
::
PrimValKind
::
*
;
match
bin_op
{
mir
::
BinOp
::
Add
=>
{
let
res
=
self
.memory.constraints
.add_binop_constraint
(
bin_op
,
left
,
right
,
left_kind
);
let
overflow
=
match
left_kind
{
U8
|
U16
|
U32
|
U64
|
U128
=>
{
self
.memory.constraints
.add_binop_constraint
(
mir
::
BinOp
::
Lt
,
res
,
left
,
left_kind
)
}
I8
|
I16
|
I32
|
I64
|
I128
=>
{
// TODO signed overflow check
PrimVal
::
from_bool
(
false
)
}
F32
|
F64
=>
{
PrimVal
::
from_bool
(
false
)
}
Bool
|
Char
|
Ptr
|
FnPtr
=>
unreachable!
()
};
Ok
((
res
,
overflow
))
}
// TODO overflow checks on other binops
_
=>
Ok
((
self
.memory.constraints
.add_binop_constraint
(
bin_op
,
left
,
right
,
left_kind
),
PrimVal
::
from_bool
(
false
)))
}
}
fn
abstract_ptr_ops
(
...
...
@@ -417,7 +439,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
_left_kind
:
PrimValKind
,
right
:
MemoryPointer
,
_right_kind
:
PrimValKind
,
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
boo
l
)
>
{
)
->
EvalResult
<
'tcx
,
(
PrimVal
,
PrimVa
l
)
>
{
use
rustc
::
mir
::
BinOp
::
*
;
use
value
::
PrimValKind
::
*
;
if
left
.alloc_id
!=
right
.alloc_id
{
...
...
@@ -429,7 +451,7 @@ impl<'a, 'tcx> EvalContext<'a, 'tcx> {
}
else
{
let
result
=
self
.memory.constraints
.add_binop_constraint
(
bin_op
,
left
.offset
.as_primval
(),
right
.offset
.as_primval
(),
U64
);
Ok
((
result
,
false
))
Ok
((
result
,
PrimVal
::
from_bool
(
false
))
)
}
}
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment