@@ -438,6 +438,15 @@ pub trait InterpreterEnv {
438438 ) -> Self :: Variable ;
439439
440440 fn set_halted ( & mut self , flag : Self :: Variable ) ;
441+
442+ fn sign_extend ( & mut self , x : & Self :: Variable , bitlength : u32 ) -> Self :: Variable {
443+ // FIXME: Constrain `high_bit`
444+ let high_bit = {
445+ let pos = self . alloc_scratch ( ) ;
446+ unsafe { self . bitmask ( x, bitlength, bitlength - 1 , pos) }
447+ } ;
448+ high_bit * Self :: constant ( ( ( 1 << ( 32 - bitlength) ) - 1 ) << bitlength) + x. clone ( )
449+ }
441450}
442451
443452pub fn interpret_instruction < Env : InterpreterEnv > ( env : & mut Env , instr : Instruction ) {
@@ -636,7 +645,8 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
636645 ITypeInstruction :: BranchGtZero => ( ) ,
637646 ITypeInstruction :: AddImmediate => {
638647 let register_rs = env. read_register ( & rs) ;
639- let res = register_rs + immediate;
648+ let offset = env. sign_extend ( & immediate, 16 ) ;
649+ let res = register_rs + offset;
640650 env. write_register ( & rt, res) ;
641651 env. set_instruction_pointer ( next_instruction_pointer. clone ( ) ) ;
642652 env. set_next_instruction_pointer ( next_instruction_pointer + Env :: constant ( 4u32 ) ) ;
@@ -646,7 +656,8 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
646656 ITypeInstruction :: AddImmediateUnsigned => {
647657 debug ! ( "Fetching register: {:?}" , rs) ;
648658 let register_rs = env. read_register ( & rs) ;
649- let res = register_rs + immediate;
659+ let offset = env. sign_extend ( & immediate, 16 ) ;
660+ let res = register_rs + offset;
650661 env. write_register ( & rt, res) ;
651662 env. set_instruction_pointer ( next_instruction_pointer. clone ( ) ) ;
652663 env. set_next_instruction_pointer ( next_instruction_pointer + Env :: constant ( 4u32 ) ) ;
@@ -670,30 +681,26 @@ pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: ITypeInstructi
670681 ITypeInstruction :: Load8 => ( ) ,
671682 ITypeInstruction :: Load16 => ( ) ,
672683 ITypeInstruction :: Load32 => {
684+ let base = env. read_register ( & rs) ;
673685 let dest = rt;
674- let addr = rs;
675- let offset = immediate;
676- let addr_with_offset = addr. clone ( ) + offset. clone ( ) ;
686+ let offset = env. sign_extend ( & immediate, 16 ) ;
687+ let addr = base. clone ( ) + offset. clone ( ) ;
677688 debug ! (
678689 "lw {:?}, {:?}({:?})" ,
679690 dest. clone( ) ,
680691 offset. clone( ) ,
681692 addr. clone( )
682693 ) ;
683694 // We load 4 bytes, i.e. one word.
684- let v0 = env. read_memory ( & addr_with_offset ) ;
685- let v1 = env. read_memory ( & ( addr_with_offset . clone ( ) + Env :: constant ( 1 ) ) ) ;
686- let v2 = env. read_memory ( & ( addr_with_offset . clone ( ) + Env :: constant ( 2 ) ) ) ;
687- let v3 = env. read_memory ( & ( addr_with_offset . clone ( ) + Env :: constant ( 3 ) ) ) ;
695+ let v0 = env. read_memory ( & addr ) ;
696+ let v1 = env. read_memory ( & ( addr . clone ( ) + Env :: constant ( 1 ) ) ) ;
697+ let v2 = env. read_memory ( & ( addr . clone ( ) + Env :: constant ( 2 ) ) ) ;
698+ let v3 = env. read_memory ( & ( addr . clone ( ) + Env :: constant ( 3 ) ) ) ;
688699 let value = ( v0 * Env :: constant ( 1 << 24 ) )
689700 + ( v1 * Env :: constant ( 1 << 16 ) )
690701 + ( v2 * Env :: constant ( 1 << 8 ) )
691702 + v3;
692- debug ! (
693- "Loaded 32 bits value from {:?}: {:?}" ,
694- addr_with_offset. clone( ) ,
695- value
696- ) ;
703+ debug ! ( "Loaded 32 bits value from {:?}: {:?}" , addr. clone( ) , value) ;
697704 env. write_register ( & dest, value) ;
698705 env. set_instruction_pointer ( next_instruction_pointer. clone ( ) ) ;
699706 env. set_next_instruction_pointer ( next_instruction_pointer + Env :: constant ( 4u32 ) ) ;
0 commit comments