diff --git a/VTIL-Architecture/VTIL-Architecture.vcxproj b/VTIL-Architecture/VTIL-Architecture.vcxproj
index d02a048..ba5d14d 100644
--- a/VTIL-Architecture/VTIL-Architecture.vcxproj
+++ b/VTIL-Architecture/VTIL-Architecture.vcxproj
@@ -24,6 +24,7 @@
+
@@ -40,11 +41,12 @@
+
+
-
diff --git a/VTIL-Architecture/VTIL-Architecture.vcxproj.filters b/VTIL-Architecture/VTIL-Architecture.vcxproj.filters
index 42fc65f..9f13a83 100644
--- a/VTIL-Architecture/VTIL-Architecture.vcxproj.filters
+++ b/VTIL-Architecture/VTIL-Architecture.vcxproj.filters
@@ -90,6 +90,9 @@
Instruction Stream
+
+ SymEx Integration
+
@@ -116,15 +119,18 @@
Virtual Machine
-
- Virtual Machine
-
Value Tracing
Value Tracing
+
+ SymEx Integration
+
+
+ SymEx Integration
+
diff --git a/VTIL-Architecture/vm/symbolic.cpp b/VTIL-Architecture/vm/symbolic.cpp
deleted file mode 100644
index b304ee2..0000000
--- a/VTIL-Architecture/vm/symbolic.cpp
+++ /dev/null
@@ -1,99 +0,0 @@
-// Copyright (c) 2020 Can Boluk and contributors of the VTIL Project
-// All rights reserved.
-//
-// Redistribution and use in source and binary forms, with or without
-// modification, are permitted provided that the following conditions are met:
-//
-// 1. Redistributions of source code must retain the above copyright notice,
-// this list of conditions and the following disclaimer.
-// 2. Redistributions in binary form must reproduce the above copyright
-// notice, this list of conditions and the following disclaimer in the
-// documentation and/or other materials provided with the distribution.
-// 3. Neither the name of VTIL Project nor the names of its contributors
-// may be used to endorse or promote products derived from this software
-// without specific prior written permission.
-//
-// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
-// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
-// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
-// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
-// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
-// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
-// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
-// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
-// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
-// POSSIBILITY OF SUCH DAMAGE.
-//
-#include "symbolic.hpp"
-
-namespace vtil
-{
- // Reads from the register.
- //
- symbolic::expression::reference symbolic_vm::read_register( const register_desc& desc )
- {
- bitcnt_t size = size_register( desc );
- register_desc full = { desc.flags, desc.local_id, size, 0, desc.architecture };
-
- auto it = register_state.find( full );
- auto exp = it == register_state.end()
- ? symbolic::CTX[ full ]
- : it->second;
-
- if ( lazy_io ) exp.make_lazy();
- if ( desc.bit_offset ) exp = exp >> desc.bit_offset;
- exp.resize( desc.bit_count );
- return lazy_io ? exp : exp.simplify();
- }
-
- // Writes to the register.
- //
- void symbolic_vm::write_register( const register_desc& desc, symbolic::expression::reference value )
- {
- bitcnt_t size = size_register( desc );
- register_desc full = { desc.flags, desc.local_id, size, 0, desc.architecture };
-
- if ( desc.bit_count == size && desc.bit_offset == 0 )
- {
- register_state.erase( desc );
- register_state.emplace( desc, std::move( value ) );
- }
- else
- {
- auto& exp = register_state[ full ];
- if ( !exp ) exp = symbolic::CTX[ full ];
- exp = ( std::move( exp ) & ~desc.get_mask() ) | ( value.resize( desc.bit_count ).resize( size ) << desc.bit_offset );
- }
- }
-
- // Reads the given number of bytes from the memory.
- //
- symbolic::expression::reference symbolic_vm::read_memory( const symbolic::expression::reference& pointer, size_t byte_count )
- {
- bitcnt_t bcnt = math::narrow_cast( byte_count * 8 );
- symbolic::expression::reference exp = memory_state.read(
- pointer,
- bcnt
- );
- if ( !exp ) return exp;
- return lazy_io ? exp.make_lazy() : exp.simplify();
- }
-
- // Writes the given expression to the memory.
- //
- bool symbolic_vm::write_memory( const symbolic::expression::reference& pointer, deferred_view value, bitcnt_t size )
- {
- return memory_state.write( pointer, value, size ).has_value();
- }
-
- // Override execute to enforce lazyness.
- //
- vm_exit_reason symbolic_vm::execute( const instruction& ins )
- {
- bool old = std::exchange( lazy_io, true );
- vm_exit_reason reason = vm_interface::execute( ins );
- lazy_io = old;
- return reason;
- }
-};
\ No newline at end of file
diff --git a/VTIL-Architecture/vm/symbolic.hpp b/VTIL-Architecture/vm/symbolic.hpp
index 1b22bb6..e5e145f 100644
--- a/VTIL-Architecture/vm/symbolic.hpp
+++ b/VTIL-Architecture/vm/symbolic.hpp
@@ -26,8 +26,10 @@
// POSSIBILITY OF SUCH DAMAGE.
//
#pragma once
+#include
#include "interface.hpp"
#include "../symex/memory.hpp"
+#include "../symex/context.hpp"
namespace vtil
{
@@ -35,38 +37,59 @@ namespace vtil
//
struct symbolic_vm : vm_interface
{
- // Flag to make I/O lazy.
- //
- bool lazy_io = false;
-
// State of the virtual machine.
//
symbolic::memory memory_state;
- std::map register_state;
+ symbolic::context register_state;
+
+ // Configuration of the virtual machine.
+ //
+ bool is_lazy = false;
+ il_const_iterator reference_iterator = symbolic::free_form_iterator;
// Reads from the register.
- // - Value will be unpacked.
//
- symbolic::expression::reference read_register( const register_desc& desc ) override;
+ symbolic::expression::reference read_register( const register_desc& desc ) override
+ {
+ return register_state.read( desc, reference_iterator );
+ }
// Writes to the register.
//
- void write_register( const register_desc& desc, symbolic::expression::reference value ) override;
+ void write_register( const register_desc& desc, symbolic::expression::reference value ) override
+ {
+ if ( is_lazy ) value.make_lazy();
+ register_state.write( desc, std::move( value ) );
+ }
// Reads the given number of bytes from the memory.
//
- symbolic::expression::reference read_memory( const symbolic::expression::reference& pointer, size_t byte_count ) override;
+ symbolic::expression::reference read_memory( const symbolic::expression::reference& pointer, size_t byte_count ) override
+ {
+ return memory_state.read( pointer, math::narrow_cast< bitcnt_t >( byte_count * 8 ), reference_iterator );
+ }
// Writes the given expression to the memory.
//
- bool write_memory( const symbolic::expression::reference& pointer, deferred_view value, bitcnt_t size ) override;
-
- // Override execute to enforce lazyness.
- //
- vm_exit_reason execute( const instruction& ins ) override;
+ bool write_memory( const symbolic::expression::reference& pointer, deferred_value value, bitcnt_t size ) override
+ {
+ if ( is_lazy )
+ {
+ deferred_result value_n = [ & ]() -> auto { return value.get().make_lazy(); };
+ return memory_state.write( pointer, value_n, size ).has_value();
+ }
+ else
+ {
+ return memory_state.write( pointer, value, size ).has_value();
+ }
+ }
// Resets the virtual machine state.
//
- void reset() { memory_state.reset(); register_state.clear(); }
+ void reset()
+ {
+ memory_state.reset();
+ register_state.reset();
+ }
};
};
\ No newline at end of file
diff --git a/VTIL-Compiler/optimizer/symbolic_rewrite_pass.cpp b/VTIL-Compiler/optimizer/symbolic_rewrite_pass.cpp
index cf4fa35..b83cd9b 100644
--- a/VTIL-Compiler/optimizer/symbolic_rewrite_pass.cpp
+++ b/VTIL-Compiler/optimizer/symbolic_rewrite_pass.cpp
@@ -127,10 +127,19 @@ namespace vtil::optimizer
//
for ( auto& pair : vm.register_state )
{
+ // Skip if not written, else collapse value.
+ // -- TODO: Will be reworked...
+ //
+ bitcnt_t msb = math::msb( pair.second.bitmap ) - 1;
+ if ( msb == -1 ) continue;
+ bitcnt_t size = pair.second.linear_store[ msb ].size() + msb;
+
+ register_desc k = { pair.first, size };
+ auto v = vm.read_register( k ).simplify();
+
// If value is unchanged, skip.
//
- auto k = pair.first; auto v = pair.second.simplify();
- symbolic::expression v0 = symbolic::CTX[ k ];
+ symbolic::expression v0 = symbolic::CTX( vm.reference_iterator )[ k ];
if ( v->equals( v0 ) )
continue;
@@ -201,9 +210,9 @@ namespace vtil::optimizer
// For each memory state:
// -- TODO: Simplify memory state, merge if simplifies, discard if left as is.
//
- for ( auto& [k, _v] : vm.memory_state )
+ for ( auto& [k, v] : vm.memory_state )
{
- auto v = _v.simplify();
+ v.simplify();
symbolic::expression v0 = symbolic::MEMORY( k, v.size() );
// If value is unchanged, skip.