Skip to content

Commit

Permalink
Development of mem SM: MemProxy, MemAlign, MemAlignRom, Mem, RomData,…
Browse files Browse the repository at this point in the history
… InputData. (#153)

* First commit on memory_checkpoint3

* Create input_data_sm.rs

* mem_proxy to little endian

* update to proofman 0.0.10

* Fix errors

* mem align working

* Write RO data sections using code instructions

* Fix riscof test by not writing RO sections with addr=0 and fixing vector index

* Ignore ELF sections with addr=0

* Mem align fully working

* Cleaning the mem align

* Removing hashmaps and cleaning up stuff a little bit

* mem - mem_align integration

* fix invalid assert on mem_align

* Remove store_c_slice to fix parallel execution without memory

* Mem align and mem fixes (#175)

* Removing unnecessary code

* update mem executors with correct call to register_predecessor

* Memory required extended data to build Memory SM proof

* Feature/custom commits (#166)

* Custom cols rom (#159)

Custom cols working

---------

Co-authored-by: Xavier Pinsach <[email protected]>

* Cached custom commits

* Updating proofman to 0.0.12

* Global constraints verifying again

* Optimizing the binary component (#167)

* Optimizing the binary

* Updating the executor

* Updating to 0.0.13

* Not creating unnecessary instances of arith tables

* Pil2-proofman 0.0.14

---------

Co-authored-by: Xavier Pinsach <[email protected]>
Co-authored-by: Héctor Masip Ardevol <[email protected]>

* remove old input_data.pil

* Zisk working with last proofman version

* Updating book and Cargo.toml to point to 0.0.16 proofman

* fix minor bug after update develop changes

* fix bug on additional mem calculation

* update direct_global continuations

* update mem pil comments

* fix last bugs on memory, added documentation

---------

Co-authored-by: Xavier Pinsach <[email protected]>
Co-authored-by: Héctor Masip <[email protected]>
Co-authored-by: zkronos73 <[email protected]>
Co-authored-by: Roger Taulé Buxadera <[email protected]>
Co-authored-by: RogerTaule <[email protected]>
  • Loading branch information
6 people authored Dec 11, 2024
1 parent a7b1300 commit e5f11b2
Show file tree
Hide file tree
Showing 45 changed files with 5,082 additions and 663 deletions.
6 changes: 3 additions & 3 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
/target
/*.tar.gz
/riscof
/build
/proofs
/build*
/proofs*
*.pilout
/tmp
*.log
*.log
4 changes: 4 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

59 changes: 48 additions & 11 deletions core/src/elf2rom.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,15 @@ pub fn elf2rom(elf_file: String) -> Result<ZiskRom, Box<dyn Error>> {
for section_header in section_headers {
// Consider only the section headers that contain program data
if section_header.sh_type == SHT_PROGBITS {
// Get the program section data as a vector of bytes
// Get the section header address
let addr = section_header.sh_addr;

// Ignore sections with address = 0, as per ELF spec
if addr == 0 {
continue;
}

// Get the section data
let (data_u8, _) = elf_bytes.section_data(&section_header)?;
let mut data = data_u8.to_vec();

Expand All @@ -37,31 +45,58 @@ pub fn elf2rom(elf_file: String) -> Result<ZiskRom, Box<dyn Error>> {
data.pop();
}

// Get the section data address
let addr = section_header.sh_addr;

// If the data contains instructions, parse them as RISC-V instructions and add them
// to the ROM instructions, at the specified program address
// If this is a code section, add it to program
if (section_header.sh_flags & SHF_EXECINSTR as u64) != 0 {
add_zisk_code(&mut rom, addr, &data);
}

// Add init data as a read/write memory section, initialized by code
// If the data is a writable memory section, add it to the ROM memory using Zisk
// copy instructions
if (section_header.sh_flags & SHF_WRITE as u64) != 0 &&
addr >= RAM_ADDR &&
addr + data.len() as u64 <= RAM_ADDR + RAM_SIZE
{
add_zisk_init_data(&mut rom, addr, &data);
// Otherwise, add it to the ROM as RO data
} else {
rom.ro_data.push(RoData::new(addr, data.len(), data));
//println! {"elf2rom() new RW from={:x} length={:x}={}", addr, data.len(),
//data.len()};
add_zisk_init_data(&mut rom, addr, &data, true);
}
// Add read-only data memory section
else {
// Search for an existing RO section previous to this one
let mut found = false;
for rd in rom.ro_data.iter_mut() {
// Section data should be previous to this one
if (rd.from + rd.length as u64) == addr {
rd.length += data.len();
rd.data.extend(data.clone());
found = true;
//println! {"elf2rom() adding RO from={:x} length={:x}={}", rd.from,
// rd.length, rd.length};
break;
}
}

// If not found, create a new RO section
if !found {
//println! {"elf2rom() new RO from={:x} length={:x}={}", addr, data.len(),
// data.len()};
rom.ro_data.push(RoData::new(addr, data.len(), data));
}
}
}
}
}

// Add the program setup, system call and program wrapup instructions
// Add RO data initialization code insctructions
let ro_data_len = rom.ro_data.len();
for i in 0..ro_data_len {
let addr = rom.ro_data[i].from;
let mut data = Vec::new();
data.extend(rom.ro_data[i].data.as_slice());
add_zisk_init_data(&mut rom, addr, &data, true);
}

add_entry_exit_jmp(&mut rom, elf_bytes.ehdr.e_entry);

// Preprocess the ROM (experimental)
Expand Down Expand Up @@ -128,6 +163,8 @@ pub fn elf2rom(elf_file: String) -> Result<ZiskRom, Box<dyn Error>> {
}
}

//println! {"elf2rom() got rom.insts.len={}", rom.insts.len()};

Ok(rom)
}

Expand Down
Loading

0 comments on commit e5f11b2

Please sign in to comment.