Skip to content
Projects
Groups
Snippets
Help
This project
Loading...
Sign in / Register
Toggle navigation
C
cwe_checker
Overview
Overview
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
fact-depend
cwe_checker
Commits
7e992eea
Unverified
Commit
7e992eea
authored
Jul 29, 2020
by
Enkelmann
Committed by
GitHub
Jul 29, 2020
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fixed ARSHIFT for shifts larger than the bitsize. (#74)
parent
7841bf89
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
239 additions
and
78 deletions
+239
-78
abstract_domain.rs
cwe_checker_rs/src/analysis/abstract_domain.rs
+45
-15
context.rs
cwe_checker_rs/src/analysis/pointer_inference/context.rs
+85
-22
data.rs
cwe_checker_rs/src/analysis/pointer_inference/data.rs
+10
-7
object.rs
cwe_checker_rs/src/analysis/pointer_inference/object.rs
+5
-1
object_list.rs
cwe_checker_rs/src/analysis/pointer_inference/object_list.rs
+17
-9
state.rs
cwe_checker_rs/src/analysis/pointer_inference/state.rs
+77
-24
No files found.
cwe_checker_rs/src/analysis/abstract_domain.rs
View file @
7e992eea
...
...
@@ -82,7 +82,7 @@ impl ValueDomain for BitvectorDomain {
use
BinOpType
::
*
;
match
op
{
LSHIFT
|
RSHIFT
|
ARSHIFT
=>
(),
_
=>
assert_eq!
(
self
.bitsize
(),
rhs
.bitsize
())
_
=>
assert_eq!
(
self
.bitsize
(),
rhs
.bitsize
()),
}
match
(
self
,
rhs
)
{
(
BitvectorDomain
::
Value
(
lhs_bitvec
),
BitvectorDomain
::
Value
(
rhs_bitvec
))
=>
match
op
{
...
...
@@ -105,10 +105,7 @@ impl ValueDomain for BitvectorDomain {
let
shift_amount
=
rhs_bitvec
.try_to_u64
()
.unwrap
()
as
usize
;
if
shift_amount
<
lhs_bitvec
.width
()
.to_usize
()
{
BitvectorDomain
::
Value
(
lhs_bitvec
.clone
()
.into_checked_shl
(
shift_amount
)
.unwrap
(),
lhs_bitvec
.clone
()
.into_checked_shl
(
shift_amount
)
.unwrap
(),
)
}
else
{
BitvectorDomain
::
Value
(
Bitvector
::
zero
(
lhs_bitvec
.width
()))
...
...
@@ -118,21 +115,29 @@ impl ValueDomain for BitvectorDomain {
let
shift_amount
=
rhs_bitvec
.try_to_u64
()
.unwrap
()
as
usize
;
if
shift_amount
<
lhs_bitvec
.width
()
.to_usize
()
{
BitvectorDomain
::
Value
(
lhs_bitvec
.clone
()
.into_checked_lshr
(
shift_amount
)
.unwrap
(),
lhs_bitvec
.clone
()
.into_checked_lshr
(
shift_amount
)
.unwrap
(),
)
}
else
{
BitvectorDomain
::
Value
(
Bitvector
::
zero
(
lhs_bitvec
.width
()))
}
}
ARSHIFT
=>
BitvectorDomain
::
Value
(
lhs_bitvec
.clone
()
.into_checked_ashr
(
rhs_bitvec
.try_to_u64
()
.unwrap
()
as
usize
)
.unwrap
(),
),
ARSHIFT
=>
{
let
shift_amount
=
rhs_bitvec
.try_to_u64
()
.unwrap
()
as
usize
;
if
shift_amount
<
lhs_bitvec
.width
()
.to_usize
()
{
BitvectorDomain
::
Value
(
lhs_bitvec
.clone
()
.into_checked_ashr
(
shift_amount
)
.unwrap
(),
)
}
else
{
let
signed_bitvec
=
apint
::
Int
::
from
(
lhs_bitvec
.clone
());
if
signed_bitvec
.is_negative
()
{
let
minus_one
=
Bitvector
::
zero
(
lhs_bitvec
.width
())
-
&
Bitvector
::
one
(
lhs_bitvec
.width
());
BitvectorDomain
::
Value
(
minus_one
)
}
else
{
BitvectorDomain
::
Value
(
Bitvector
::
zero
(
lhs_bitvec
.width
()))
}
}
}
AND
=>
BitvectorDomain
::
Value
(
lhs_bitvec
&
rhs_bitvec
),
OR
=>
BitvectorDomain
::
Value
(
lhs_bitvec
|
rhs_bitvec
),
XOR
=>
BitvectorDomain
::
Value
(
lhs_bitvec
^
rhs_bitvec
),
...
...
@@ -362,4 +367,29 @@ mod tests {
assert
!
(
!
bv
(
17
)
.is_top
());
assert
!
(
BitvectorDomain
::
new_top
(
64
)
.is_top
());
}
#[test]
fn
arshift
()
{
use
crate
::
bil
::
BinOpType
::
ARSHIFT
;
let
positive_x
=
BitvectorDomain
::
Value
(
Bitvector
::
from_i64
(
31
));
let
negative_x
=
BitvectorDomain
::
Value
(
Bitvector
::
from_i64
(
-
31
));
let
shift_3
=
BitvectorDomain
::
Value
(
Bitvector
::
from_u8
(
3
));
let
shift_70
=
BitvectorDomain
::
Value
(
Bitvector
::
from_u8
(
70
));
assert_eq!
(
positive_x
.bin_op
(
ARSHIFT
,
&
shift_3
),
BitvectorDomain
::
Value
(
Bitvector
::
from_i64
(
3
))
);
assert_eq!
(
positive_x
.bin_op
(
ARSHIFT
,
&
shift_70
),
BitvectorDomain
::
Value
(
Bitvector
::
from_i64
(
0
))
);
assert_eq!
(
negative_x
.bin_op
(
ARSHIFT
,
&
shift_3
),
BitvectorDomain
::
Value
(
Bitvector
::
from_i64
(
-
4
))
);
assert_eq!
(
negative_x
.bin_op
(
ARSHIFT
,
&
shift_70
),
BitvectorDomain
::
Value
(
Bitvector
::
from_i64
(
-
1
))
);
}
}
cwe_checker_rs/src/analysis/pointer_inference/context.rs
View file @
7e992eea
...
...
@@ -214,7 +214,9 @@ impl<'a> crate::analysis::interprocedural_fixpoint::Problem<'a> for Context<'a>
);
// set the list of caller stack ids to only this caller id
callee_state
.caller_stack_ids
=
BTreeSet
::
new
();
callee_state
.caller_stack_ids
.insert
(
new_caller_stack_id
.clone
());
callee_state
.caller_stack_ids
.insert
(
new_caller_stack_id
.clone
());
// Remove non-referenced objects and objects, only the caller knows about, from the state.
callee_state
.ids_known_to_caller
=
BTreeSet
::
new
();
callee_state
.remove_unreferenced_objects
();
...
...
@@ -255,7 +257,10 @@ impl<'a> crate::analysis::interprocedural_fixpoint::Problem<'a> for Context<'a>
// Check whether state_before_return actually knows the caller_stack_id.
// If not, we are returning from a state that cannot correspond to this callsite.
if
!
state_before_return
.caller_stack_ids
.contains
(
&
caller_stack_id
)
{
if
!
state_before_return
.caller_stack_ids
.contains
(
&
caller_stack_id
)
{
return
None
;
}
...
...
@@ -541,7 +546,7 @@ mod tests {
}
fn
reg_add_term
(
name
:
&
str
,
value
:
i64
,
tid_name
:
&
str
)
->
Term
<
Def
>
{
let
add_expr
=
Expression
::
BinOp
{
let
add_expr
=
Expression
::
BinOp
{
op
:
crate
::
bil
::
BinOpType
::
PLUS
,
lhs
:
Box
::
new
(
Expression
::
Var
(
register
(
name
))),
rhs
:
Box
::
new
(
Expression
::
Const
(
Bitvector
::
from_i64
(
value
))),
...
...
@@ -551,7 +556,7 @@ mod tests {
term
:
Def
{
lhs
:
register
(
name
),
rhs
:
add_expr
,
}
}
,
}
}
...
...
@@ -763,34 +768,81 @@ mod tests {
#[test]
fn
update_return
()
{
use
crate
::
analysis
::
interprocedural_fixpoint
::
Problem
;
use
crate
::
analysis
::
pointer_inference
::
object
::
ObjectType
;
use
crate
::
analysis
::
pointer_inference
::
data
::
*
;
use
crate
::
analysis
::
pointer_inference
::
object
::
ObjectType
;
let
project
=
mock_project
();
let
(
cwe_sender
,
_cwe_receiver
)
=
crossbeam_channel
::
unbounded
();
let
(
log_sender
,
_log_receiver
)
=
crossbeam_channel
::
unbounded
();
let
context
=
Context
::
new
(
&
project
,
cwe_sender
,
log_sender
);
let
state_before_return
=
State
::
new
(
&
register
(
"RSP"
),
Tid
::
new
(
"callee"
));
let
mut
state_before_return
=
context
.update_def
(
&
state_before_return
,
&
reg_add_term
(
"RSP"
,
8
,
"stack_offset_on_return_adjustment"
));
let
mut
state_before_return
=
context
.update_def
(
&
state_before_return
,
&
reg_add_term
(
"RSP"
,
8
,
"stack_offset_on_return_adjustment"
),
);
let
callsite_id
=
new_id
(
"call_callee"
,
"RSP"
);
state_before_return
.memory
.add_abstract_object
(
callsite_id
.clone
(),
bv
(
0
)
.into
(),
ObjectType
::
Stack
,
64
);
state_before_return
.caller_stack_ids
.insert
(
callsite_id
.clone
());
state_before_return
.ids_known_to_caller
.insert
(
callsite_id
.clone
());
state_before_return
.memory
.add_abstract_object
(
callsite_id
.clone
(),
bv
(
0
)
.into
(),
ObjectType
::
Stack
,
64
,
);
state_before_return
.caller_stack_ids
.insert
(
callsite_id
.clone
());
state_before_return
.ids_known_to_caller
.insert
(
callsite_id
.clone
());
let
other_callsite_id
=
new_id
(
"call_callee_other"
,
"RSP"
);
state_before_return
.memory
.add_abstract_object
(
other_callsite_id
.clone
(),
bv
(
0
)
.into
(),
ObjectType
::
Stack
,
64
);
state_before_return
.caller_stack_ids
.insert
(
other_callsite_id
.clone
());
state_before_return
.ids_known_to_caller
.insert
(
other_callsite_id
.clone
());
state_before_return
.set_register
(
&
register
(
"RAX"
),
Data
::
Pointer
(
PointerDomain
::
new
(
new_id
(
"call_callee_other"
,
"RSP"
),
bv
(
-
32
))))
.unwrap
();
state_before_return
.memory
.add_abstract_object
(
other_callsite_id
.clone
(),
bv
(
0
)
.into
(),
ObjectType
::
Stack
,
64
,
);
state_before_return
.caller_stack_ids
.insert
(
other_callsite_id
.clone
());
state_before_return
.ids_known_to_caller
.insert
(
other_callsite_id
.clone
());
state_before_return
.set_register
(
&
register
(
"RAX"
),
Data
::
Pointer
(
PointerDomain
::
new
(
new_id
(
"call_callee_other"
,
"RSP"
),
bv
(
-
32
),
)),
)
.unwrap
();
let
state_before_call
=
State
::
new
(
&
register
(
"RSP"
),
Tid
::
new
(
"original_caller_id"
));
let
mut
state_before_call
=
context
.update_def
(
&
state_before_call
,
&
reg_add_term
(
"RSP"
,
-
16
,
"stack_offset_on_call_adjustment"
));
let
mut
state_before_call
=
context
.update_def
(
&
state_before_call
,
&
reg_add_term
(
"RSP"
,
-
16
,
"stack_offset_on_call_adjustment"
),
);
let
caller_caller_id
=
new_id
(
"caller_caller"
,
"RSP"
);
state_before_call
.memory
.add_abstract_object
(
caller_caller_id
.clone
(),
bv
(
0
)
.into
(),
ObjectType
::
Stack
,
64
);
state_before_call
.caller_stack_ids
.insert
(
caller_caller_id
.clone
());
state_before_call
.ids_known_to_caller
.insert
(
caller_caller_id
.clone
());
let
state
=
context
.update_return
(
&
state_before_return
,
Some
(
&
state_before_call
),
&
call_term
(
"callee"
))
.unwrap
();
state_before_call
.memory
.add_abstract_object
(
caller_caller_id
.clone
(),
bv
(
0
)
.into
(),
ObjectType
::
Stack
,
64
,
);
state_before_call
.caller_stack_ids
.insert
(
caller_caller_id
.clone
());
state_before_call
.ids_known_to_caller
.insert
(
caller_caller_id
.clone
());
let
state
=
context
.update_return
(
&
state_before_return
,
Some
(
&
state_before_call
),
&
call_term
(
"callee"
),
)
.unwrap
();
let
mut
caller_caller_set
=
BTreeSet
::
new
();
caller_caller_set
.insert
(
caller_caller_id
);
...
...
@@ -799,10 +851,21 @@ mod tests {
assert_eq!
(
state
.stack_id
,
new_id
(
"original_caller_id"
,
"RSP"
));
assert
!
(
state_before_return
.memory
.get_all_object_ids
()
.len
()
==
3
);
assert
!
(
state
.memory
.get_all_object_ids
()
.len
()
==
2
);
assert
!
(
state
.memory
.get_all_object_ids
()
.get
(
&
new_id
(
"original_caller_id"
,
"RSP"
))
.is_some
());
assert
!
(
state
.memory
.get_all_object_ids
()
.get
(
&
new_id
(
"caller_caller"
,
"RSP"
))
.is_some
());
assert
!
(
state
.memory
.get_all_object_ids
()
.get
(
&
new_id
(
"original_caller_id"
,
"RSP"
))
.is_some
());
assert
!
(
state
.memory
.get_all_object_ids
()
.get
(
&
new_id
(
"caller_caller"
,
"RSP"
))
.is_some
());
assert
!
(
state
.get_register
(
&
register
(
"RSP"
))
.is_ok
());
let
expected_rsp
=
Data
::
Pointer
(
PointerDomain
::
new
(
new_id
(
"original_caller_id"
,
"RSP"
),
bv
(
-
8
)));
let
expected_rsp
=
Data
::
Pointer
(
PointerDomain
::
new
(
new_id
(
"original_caller_id"
,
"RSP"
),
bv
(
-
8
),
));
assert_eq!
(
state
.get_register
(
&
register
(
"RSP"
))
.unwrap
(),
expected_rsp
);
}
}
cwe_checker_rs/src/analysis/pointer_inference/data.rs
View file @
7e992eea
...
...
@@ -44,13 +44,16 @@ impl Data {
pub
fn
remove_ids
(
&
mut
self
,
ids_to_remove
:
&
BTreeSet
<
AbstractIdentifier
>
)
{
// TODO: Some callers don't want to get Top(..) values. Probably has to be handled at the respective callsites.
if
let
Data
::
Pointer
(
pointer
)
=
self
{
let
remaining_targets
:
BTreeMap
<
AbstractIdentifier
,
BitvectorDomain
>
=
pointer
.iter_targets
()
.filter_map
(|(
id
,
offset
)|
{
if
ids_to_remove
.get
(
id
)
.is_none
()
{
Some
((
id
.clone
(),
offset
.clone
()))
}
else
{
None
}
})
.collect
();
let
remaining_targets
:
BTreeMap
<
AbstractIdentifier
,
BitvectorDomain
>
=
pointer
.iter_targets
()
.filter_map
(|(
id
,
offset
)|
{
if
ids_to_remove
.get
(
id
)
.is_none
()
{
Some
((
id
.clone
(),
offset
.clone
()))
}
else
{
None
}
})
.collect
();
if
remaining_targets
.len
()
==
0
{
*
self
=
Data
::
new_top
(
self
.bitsize
());
}
else
{
...
...
cwe_checker_rs/src/analysis/pointer_inference/object.rs
View file @
7e992eea
...
...
@@ -255,7 +255,11 @@ impl AbstractObjectInfo {
/// Remove the provided IDs from the target lists of all pointers in the memory object.
/// Also remove them from the pointer_targets list.
pub
fn
remove_ids
(
&
mut
self
,
ids_to_remove
:
&
BTreeSet
<
AbstractIdentifier
>
)
{
self
.pointer_targets
=
self
.pointer_targets
.difference
(
ids_to_remove
)
.cloned
()
.collect
();
self
.pointer_targets
=
self
.pointer_targets
.difference
(
ids_to_remove
)
.cloned
()
.collect
();
for
value
in
self
.memory
.iter_values_mut
()
{
value
.remove_ids
(
ids_to_remove
);
}
...
...
cwe_checker_rs/src/analysis/pointer_inference/object_list.rs
View file @
7e992eea
...
...
@@ -383,12 +383,16 @@ impl AbstractObjectList {
for
old_index
in
0
..
other_object_list
.objects
.len
()
{
if
objects_already_known
[
old_index
]
==
false
{
old_to_new_index_map
.insert
(
old_index
,
self
.objects
.len
());
self
.objects
.push
(
other_object_list
.objects
[
old_index
]
.clone
());
self
.objects
.push
(
other_object_list
.objects
[
old_index
]
.clone
());
}
}
for
(
id
,
(
old_index
,
offset
))
in
other_object_list
.ids
.iter
()
{
if
old_to_new_index_map
.get
(
old_index
)
.is_some
()
{
self
.ids
.insert
(
id
.clone
(),
(
old_to_new_index_map
[
old_index
],
offset
.clone
()));
self
.ids
.insert
(
id
.clone
(),
(
old_to_new_index_map
[
old_index
],
offset
.clone
()),
);
}
}
}
...
...
@@ -403,13 +407,17 @@ impl AbstractObjectList {
let
object
=
Arc
::
make_mut
(
object
);
object
.remove_ids
(
ids_to_remove
);
}
self
.ids
=
self
.ids
.iter
()
.filter_map
(|(
id
,
(
index
,
offset
))|
{
if
ids_to_remove
.get
(
id
)
.is_none
()
{
Some
((
id
.clone
(),
(
*
index
,
offset
.clone
())))
}
else
{
None
}
})
.collect
();
self
.ids
=
self
.ids
.iter
()
.filter_map
(|(
id
,
(
index
,
offset
))|
{
if
ids_to_remove
.get
(
id
)
.is_none
()
{
Some
((
id
.clone
(),
(
*
index
,
offset
.clone
())))
}
else
{
None
}
})
.collect
();
}
}
...
...
cwe_checker_rs/src/analysis/pointer_inference/state.rs
View file @
7e992eea
...
...
@@ -364,8 +364,16 @@ impl State {
register
:
merged_register
,
memory
:
merged_memory_objects
,
stack_id
:
self
.stack_id
.clone
(),
caller_stack_ids
:
self
.caller_stack_ids
.union
(
&
other
.caller_stack_ids
)
.cloned
()
.collect
(),
ids_known_to_caller
:
self
.ids_known_to_caller
.union
(
&
other
.ids_known_to_caller
)
.cloned
()
.collect
(),
caller_stack_ids
:
self
.caller_stack_ids
.union
(
&
other
.caller_stack_ids
)
.cloned
()
.collect
(),
ids_known_to_caller
:
self
.ids_known_to_caller
.union
(
&
other
.ids_known_to_caller
)
.cloned
()
.collect
(),
}
}
...
...
@@ -384,7 +392,9 @@ impl State {
if
*
id
==
self
.stack_id
{
match
offset
{
BitvectorDomain
::
Value
(
offset_val
)
=>
{
if
offset_val
.try_to_i64
()
.unwrap
()
>=
0
&&
self
.caller_stack_ids
.len
()
>
0
{
if
offset_val
.try_to_i64
()
.unwrap
()
>=
0
&&
self
.caller_stack_ids
.len
()
>
0
{
for
caller_id
in
self
.caller_stack_ids
.iter
()
{
new_targets
.add_target
(
caller_id
.clone
(),
offset
.clone
());
}
...
...
@@ -535,7 +545,11 @@ impl State {
self
.memory
.remove_ids
(
&
ids_to_remove
);
self
.caller_stack_ids
=
BTreeSet
::
new
();
self
.caller_stack_ids
.insert
(
caller_id
.clone
());
self
.ids_known_to_caller
=
self
.ids_known_to_caller
.difference
(
&
ids_to_remove
)
.cloned
()
.collect
();
self
.ids_known_to_caller
=
self
.ids_known_to_caller
.difference
(
&
ids_to_remove
)
.cloned
()
.collect
();
}
/// Add those objects from the caller_state to self, that are not known to self.
...
...
@@ -609,7 +623,7 @@ mod tests {
}
fn
reg_add
(
name
:
&
str
,
value
:
i64
)
->
Expression
{
Expression
::
BinOp
{
Expression
::
BinOp
{
op
:
BinOpType
::
PLUS
,
lhs
:
Box
::
new
(
Expression
::
Var
(
register
(
name
))),
rhs
:
Box
::
new
(
Expression
::
Const
(
Bitvector
::
from_i64
(
value
))),
...
...
@@ -617,7 +631,7 @@ mod tests {
}
fn
reg_sub
(
name
:
&
str
,
value
:
i64
)
->
Expression
{
Expression
::
BinOp
{
Expression
::
BinOp
{
op
:
BinOpType
::
MINUS
,
lhs
:
Box
::
new
(
Expression
::
Var
(
register
(
name
))),
rhs
:
Box
::
new
(
Expression
::
Const
(
Bitvector
::
from_i64
(
value
))),
...
...
@@ -627,11 +641,14 @@ mod tests {
fn
store_exp
(
address
:
Expression
,
value
:
Expression
)
->
Expression
{
let
mem_var
=
Variable
{
name
:
"mem"
.into
(),
type_
:
crate
::
bil
::
variable
::
Type
::
Memory
{
addr_size
:
64
,
elem_size
:
64
},
type_
:
crate
::
bil
::
variable
::
Type
::
Memory
{
addr_size
:
64
,
elem_size
:
64
,
},
is_temp
:
false
,
};
Expression
::
Store
{
memory
:
Box
::
new
(
Expression
::
Var
(
mem_var
)),
Expression
::
Store
{
memory
:
Box
::
new
(
Expression
::
Var
(
mem_var
)),
address
:
Box
::
new
(
address
),
value
:
Box
::
new
(
value
),
endian
:
Endianness
::
LittleEndian
,
...
...
@@ -642,11 +659,14 @@ mod tests {
fn
load_exp
(
address
:
Expression
)
->
Expression
{
let
mem_var
=
Variable
{
name
:
"mem"
.into
(),
type_
:
crate
::
bil
::
variable
::
Type
::
Memory
{
addr_size
:
64
,
elem_size
:
64
},
type_
:
crate
::
bil
::
variable
::
Type
::
Memory
{
addr_size
:
64
,
elem_size
:
64
,
},
is_temp
:
false
,
};
Expression
::
Load
{
memory
:
Box
::
new
(
Expression
::
Var
(
mem_var
)),
Expression
::
Load
{
memory
:
Box
::
new
(
Expression
::
Var
(
mem_var
)),
address
:
Box
::
new
(
address
),
endian
:
Endianness
::
LittleEndian
,
size
:
64
,
...
...
@@ -749,20 +769,53 @@ mod tests {
use
crate
::
bil
::
Expression
::
*
;
let
mut
state
=
State
::
new
(
&
register
(
"RSP"
),
Tid
::
new
(
"time0"
));
let
stack_id
=
new_id
(
"RSP"
.into
());
assert_eq!
(
state
.eval
(
&
Var
(
register
(
"RSP"
)))
.unwrap
(),
Data
::
Pointer
(
PointerDomain
::
new
(
stack_id
.clone
(),
bv
(
0
))));
assert_eq!
(
state
.eval
(
&
Var
(
register
(
"RSP"
)))
.unwrap
(),
Data
::
Pointer
(
PointerDomain
::
new
(
stack_id
.clone
(),
bv
(
0
)))
);
state
.handle_register_assign
(
&
register
(
"RSP"
),
&
reg_sub
(
"RSP"
,
32
))
.unwrap
();
assert_eq!
(
state
.eval
(
&
Var
(
register
(
"RSP"
)))
.unwrap
(),
Data
::
Pointer
(
PointerDomain
::
new
(
stack_id
.clone
(),
bv
(
-
32
))));
state
.handle_register_assign
(
&
register
(
"RSP"
),
&
reg_add
(
"RSP"
,
-
8
))
.unwrap
();
assert_eq!
(
state
.eval
(
&
Var
(
register
(
"RSP"
)))
.unwrap
(),
Data
::
Pointer
(
PointerDomain
::
new
(
stack_id
.clone
(),
bv
(
-
40
))));
state
.handle_register_assign
(
&
register
(
"RSP"
),
&
reg_sub
(
"RSP"
,
32
))
.unwrap
();
assert_eq!
(
state
.eval
(
&
Var
(
register
(
"RSP"
)))
.unwrap
(),
Data
::
Pointer
(
PointerDomain
::
new
(
stack_id
.clone
(),
bv
(
-
32
)))
);
state
.handle_register_assign
(
&
register
(
"RSP"
),
&
reg_add
(
"RSP"
,
-
8
))
.unwrap
();
assert_eq!
(
state
.eval
(
&
Var
(
register
(
"RSP"
)))
.unwrap
(),
Data
::
Pointer
(
PointerDomain
::
new
(
stack_id
.clone
(),
bv
(
-
40
)))
);
state
.handle_store_exp
(
&
store_exp
(
reg_add
(
"RSP"
,
8
),
Const
(
Bitvector
::
from_i64
(
1
))))
.unwrap
();
state
.handle_store_exp
(
&
store_exp
(
reg_sub
(
"RSP"
,
8
),
Const
(
Bitvector
::
from_i64
(
2
))))
.unwrap
();
state
.handle_store_exp
(
&
store_exp
(
reg_add
(
"RSP"
,
-
16
),
Const
(
Bitvector
::
from_i64
(
3
))))
.unwrap
();
state
.handle_register_assign
(
&
register
(
"RSP"
),
&
reg_sub
(
"RSP"
,
4
))
.unwrap
();
state
.handle_store_exp
(
&
store_exp
(
reg_add
(
"RSP"
,
8
),
Const
(
Bitvector
::
from_i64
(
1
))))
.unwrap
();
state
.handle_store_exp
(
&
store_exp
(
reg_sub
(
"RSP"
,
8
),
Const
(
Bitvector
::
from_i64
(
2
))))
.unwrap
();
state
.handle_store_exp
(
&
store_exp
(
reg_add
(
"RSP"
,
-
16
),
Const
(
Bitvector
::
from_i64
(
3
)),
))
.unwrap
();
state
.handle_register_assign
(
&
register
(
"RSP"
),
&
reg_sub
(
"RSP"
,
4
))
.unwrap
();
assert_eq!
(
state
.eval
(
&
load_exp
(
reg_add
(
"RSP"
,
12
)))
.unwrap
(),
bv
(
1
)
.into
());
assert_eq!
(
state
.eval
(
&
load_exp
(
reg_sub
(
"RSP"
,
4
)))
.unwrap
(),
bv
(
2
)
.into
());
assert_eq!
(
state
.eval
(
&
load_exp
(
reg_add
(
"RSP"
,
-
12
)))
.unwrap
(),
bv
(
3
)
.into
());
assert_eq!
(
state
.eval
(
&
load_exp
(
reg_add
(
"RSP"
,
12
)))
.unwrap
(),
bv
(
1
)
.into
()
);
assert_eq!
(
state
.eval
(
&
load_exp
(
reg_sub
(
"RSP"
,
4
)))
.unwrap
(),
bv
(
2
)
.into
()
);
assert_eq!
(
state
.eval
(
&
load_exp
(
reg_add
(
"RSP"
,
-
12
)))
.unwrap
(),
bv
(
3
)
.into
()
);
}
}
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment