Update Artifact with missing changes for hardware generation

.gitmodules

@@ -1,24 +1,24 @@
 [submodule "lib/codegen"]
     path = lib/codegen
-    url = git@github.com:achreto/codegen-rs.git
+    url = https://github.com/achreto/codegen-rs.git
 [submodule "lib/crustal"]
 	path = lib/crustal
-	url = git@github.com:achreto/crustal.git
+	url = https://github.com/achreto/crustal.git
 [submodule "lib/smtlib2"]
 	path = lib/smtlib2
-	url = git@github.com:achreto/rust-smtlib2.git
+	url = https://github.com/achreto/rust-smtlib2.git
 [submodule "lib/srcspan"]
 	path = lib/srcspan
-	url = git@github.com:achreto/rust-srcspan.git
+	url = https://github.com/achreto/rust-srcspan.git
 [submodule "lib/tokstream"]
 	path = lib/tokstream
-	url = git@github.com:achreto/rust-tokstream.git
+	url = https://github.com/achreto/rust-tokstream.git
 [submodule "lib/z3"]
 	path = lib/z3
-	url = git@github.com:achreto/z3.rs.git
+	url = https://github.com/achreto/z3.rs.git
 [submodule "support/arm-fastmodels-boot"]
 	path = support/arm-fastmodels-boot
-	url = git@github.com:achreto/arm-fastmodels-boot.git
+	url = https://github.com/achreto/arm-fastmodels-boot.git
 [submodule "lib/velosiraptor-parser"]
 	path = lib/velosiraptor-parser
-	url = git@github.com:ubc-systopia/velosiraptor-parser.git
+	url = https://github.com/ubc-systopia/velosiraptor-parser.git

benches/runtime/bench.c

@@ -122,9 +122,9 @@ int main() {
 
     x8664pml4__t vroot;
     x8664pml4_alloc(&vroot);
-    run_benchmark("Arbutus-x86_64-Map", velosiraptor_map_one, &vroot, vaddr, paddr);
-    run_benchmark("Arbutus-x86_64-Protect", velosiraptor_protect_one,  &vroot, vaddr, paddr);
-    run_benchmark("Arbutus-x86_64-Unmap", velosiraptor_unmap_one,  &vroot, vaddr, paddr);
+    run_benchmark("Velosiraptor-x86_64-Map", velosiraptor_map_one, &vroot, vaddr, paddr);
+    run_benchmark("Velosiraptor-x86_64-Protect", velosiraptor_protect_one,  &vroot, vaddr, paddr);
+    run_benchmark("Velosiraptor-x86_64-Unmap", velosiraptor_unmap_one,  &vroot, vaddr, paddr);
 
 
     void *st = barrelfish_init();
@@ -134,8 +134,8 @@ int main() {
 
     x8664pagetable__t pt;
     x8664pagetable_alloc(&pt);
-    run_benchmark("Arbutus-PTable-Map", velosiraptor_pte_map, &pt, vaddr, paddr);
-    run_benchmark("Arbutus-PTable-Protect", velosiraptor_pte_protect,  &pt, vaddr, paddr);
-    run_benchmark("Arbutus-PTable-Unmap", velosiraptor_pte_unmap,  &pt, vaddr, paddr);
+    run_benchmark("Velosiraptor-PTable-Map", velosiraptor_pte_map, &pt, vaddr, paddr);
+    run_benchmark("Velosiraptor-PTable-Protect", velosiraptor_pte_protect,  &pt, vaddr, paddr);
+    run_benchmark("Velosiraptor-PTable-Unmap", velosiraptor_pte_unmap,  &pt, vaddr, paddr);
 
 }

benches/runtime/main.rs

@@ -25,9 +25,9 @@ use bench::*;
 
 const ROWS: [&str; 4] = [
     "Linux-x86_64",
-    "Arbutus-x86_64",
+    "Velosiraptor-x86_64",
     "Barrelfish-PTable",
-    "Arbutus-PTable",
+    "Velosiraptor-PTable",
 ];
 
 const COLS: [&str; 3] = ["Map", "Protect", "Unmap"];

benches/synth/bench.rs

@@ -1,4 +1,4 @@
-pub const NUM_WORKERS: usize = 13; // give one core to the main program...
+pub const NUM_WORKERS: usize = 23; // give one core to the main program...
 pub const ITERATIONS: usize = 100;
 
 pub struct Stats {

benches/synth/main.rs

@@ -211,7 +211,7 @@ const LINUX_GIT_URL: &str =
     "https://git.launchpad.net/~ubuntu-kernel/ubuntu/+source/linux/+git/noble";
 const LINUX_GIT_SHA: &str = "74134bfb6b720ca18a73931662cbcc8170ef1bed";
 
-fn compile_linux(nworkers: usize) -> Option<Stats> {
+fn compile_linux(nworkers: usize, iterations: usize) -> Option<Stats> {
     println!("Running Linux Compilation Benchmark");
 
     let config_file = Path::new(file!()).parent().unwrap().join("ubuntu.config");
@@ -290,7 +290,7 @@ fn compile_linux(nworkers: usize) -> Option<Stats> {
         .output()
         .expect("failed to execute process");
 
-    let bar = ProgressBar::new(ITERATIONS.try_into().unwrap());
+    let bar = ProgressBar::new(iterations.try_into().unwrap());
     bar.set_style(
         ProgressStyle::with_template(
             "{spinner:.dim.bold} [{bar:40.cyan/blue}]  {pos}/{len}  -  {msg:20}",
@@ -300,8 +300,8 @@ fn compile_linux(nworkers: usize) -> Option<Stats> {
     );
 
     let parallelism = format!("-j{}", nworkers);
-    let mut measurements = Vec::with_capacity(ITERATIONS);
-    for _ in 0..ITERATIONS {
+    let mut measurements = Vec::with_capacity(iterations);
+    for _ in 0..iterations {
         bar.set_message("make clean");
         // println!(" - Running make clean");
         Command::new("make")
@@ -346,6 +346,7 @@ fn main() {
     let is_dirty = !output.stdout.is_empty();
     let build_dirty = env!("VERGEN_GIT_DIRTY") == "true";
     let allow_dirty = args.iter().any(|e| e.as_str() == "--allow-dirty");
+    let is_smoke = args.iter().any(|e| e.as_str() == "--smoke");
 
     if is_dirty && !allow_dirty {
         println!("ERROR. Git repository is dirty. Terminating.");
@@ -362,10 +363,8 @@ fn main() {
     let mut latex_results = String::new();
     let mut latex_results_no_tree = String::new();
 
-    let nworkers = std::cmp::max(
-        if nthreads > 1 { (nthreads / 2) - 1 } else { 1 },
-        NUM_WORKERS,
-    );
+    let nworkers = if nthreads > 1 { (nthreads / 2) - 1 } else { 1 };
+    let iterations = if is_smoke { 5 } else { ITERATIONS };
     for (spec, name) in SPECS.iter() {
         println!(" @ Spec: {spec}");
 
@@ -387,7 +386,7 @@ fn main() {
             let mut results = BenchResults::new(name.to_string());
             let mut had_errors = false;
             print!("    ");
-            let bar = ProgressBar::new(ITERATIONS.try_into().unwrap());
+            let bar = ProgressBar::new(iterations.try_into().unwrap());
             bar.set_style(
                 ProgressStyle::with_template(
                     "{spinner:.dim.bold} [{bar:40.cyan/blue}]  {pos}/{len}  -  {msg:20}",
@@ -396,7 +395,7 @@ fn main() {
                 .tick_chars("/|\\- "),
             );
 
-            for _ in 0..ITERATIONS {
+            for _ in 0..iterations {
                 // create synth factory and run synthesis on the segments
                 let mut z3_workers = Z3WorkerPool::with_num_workers(nworkers, None);
                 if let Some(res) = run_synthesis(
@@ -445,7 +444,7 @@ fn main() {
     }
     latex_results.push_str("  \\hline % ---------------------------------------------------------------------------------");
 
-    let linux_times = compile_linux(nthreads);
+    let linux_times = compile_linux(nthreads, iterations);
 
     println!("# Completed\n\n");
 
@@ -468,7 +467,7 @@ fn main() {
     println!("% Date:       {}", Local::now());
     println!("% Threads:    {}", nthreads);
     println!("% Workers:    {}", nworkers);
-    println!("% Iterations: {}", ITERATIONS);
+    println!("% Iterations: {}", iterations);
     println!(
         "% =========================================================================================="
     );

examples/assoc_segment.vrs

@@ -53,7 +53,7 @@ segment AssocSegment(base : addr) {
         mmio dst [ base, 0, 8 ],
         mmio src [ base, 8, 8 ],
         mmio length [ base, 16, 8 ],
-        mmio perms [ base, 16, 8 ],
+        mmio perms [ base, 24, 8 ],
     }
 
     // add the valid bit

examples/mpu.vrs

@@ -57,24 +57,24 @@ segment MPU(base: addr) {
             // 4 .. 5 _res, // reserved
             5 .. 32 limit   // limit
         },
-        reg rbar_a1 [ 4 ] {
-            0..32 _res,
-        },
-        reg rlar_a1 [ 4 ] {
-            0..32 _res,
-        },
-        reg rbar_a2 [ 4 ] {
-            0..32 _res,
-        },
-        reg rlar_a2 [ 4 ] {
-            0..32 _res,
-        },
-        reg rbar_a3 [ 4 ] {
-            0..32 _res,
-        },
-        reg rlar_a3 [ 4 ] {
-            0..32 _res,
-        },
+        // reg rbar_a1 [ 4 ] {
+        //     0..32 _res,
+        // },
+        // reg rlar_a1 [ 4 ] {
+        //     0..32 _res,
+        // },
+        // reg rbar_a2 [ 4 ] {
+        //     0..32 _res,
+        // },
+        // reg rlar_a2 [ 4 ] {
+        //     0..32 _res,
+        // },
+        // reg rbar_a3 [ 4 ] {
+        //     0..32 _res,
+        // },
+        // reg rlar_a3 [ 4 ] {
+        //     0..32 _res,
+        // },
         reg mair0 [ 4 ] {
              0 ..  8 attr0,
              8 .. 16 attr1,

examples/multisegment.vrs

@@ -63,7 +63,7 @@ segment SingleSegment(base : addr) {
     fn translate(va: vaddr) -> paddr
         requires va < PAGE_SIZE
     {
-        va + state.seg.address << 4
+        va + (state.seg.address << 4)
     }
 
     synth fn map(va: vaddr, sz: size, flgs: flags, pa : paddr)
@@ -83,6 +83,6 @@ segment SingleSegment(base : addr) {
 
 
 // represents an x86 page directory entry
-staticmap X8632PageDirectory(base : paddr) {
+staticmap MultiSegment(base : paddr) {
     maps [ SingleSegment(base + i * 8) for i in 0..NUM_REGIONS ]
 }

examples/simple_translation_table.vrs

@@ -146,7 +146,7 @@ segment X86_MMU(base: paddr) {
     fn translate(va: vaddr) -> paddr
         requires va < VSPACE_ADDR_MAX
     {
-        va + (state.ttbr.address << 12)
+        (state.ttbr.address << 12)
     }
 
     synth fn map(va: vaddr, sz: size, flgs: flags, pa : PageTable)

examples/x86_32_pagetable.vrs

@@ -309,7 +309,7 @@ segment X8632PageDirectoryEntryTable(base : paddr) {
     fn translate(va: vaddr) -> paddr
         requires state.entry.pagesize == 0
     {
-        va + (state.entry.address << 12)
+        (state.entry.address << 12)
     }
 
     // unmapping an entry
@@ -372,7 +372,7 @@ segment X86MMU(base: paddr) {
     fn translate(va: vaddr) -> paddr
     {
         if state.cr4.enabled == 1 {
-            va + (state.cr3.address << 12)
+            (state.cr3.address << 12)
         } else {
             va
         }

examples/x86_64_pagetable.vrs

@@ -92,7 +92,7 @@ abstract segment X8664PTableDescriptor(base: paddr) {
     fn translate(va: vaddr) -> paddr
         requires state.entry.ps == 0
     {
-        (state.entry.address << 12)
+        state.entry.address << BASE_PAGE_BITS
     }
 }
 
@@ -461,7 +461,7 @@ segment X86MMU(base: paddr) {
         requires va < VSPACE_SIZE
     {
         if state.cr4.enabled == 1 {
-            va + (state.cr3.address << 12)
+            state.cr3.address << BASE_PAGE_BITS
         } else {
             va
         }

examples/x86_segmentation.vrs

@@ -36,11 +36,11 @@ abstract segment SegmentDescriptorBase(base: addr) {
 
 
     state(base: addr) {
-        mem entry_lo [ base, 0, 4 ] {
+        reg entry_lo [ 4 ] {
             0  .. 16 limit0,  // segment limit [15:0]
             16 .. 32 base0,   // base[15:0]
         },
-        mem entry_hi [ base, 4, 4 ] {
+        reg entry_hi [ 4 ] {
              0 ..  8  base1,  // base[16:23]
              8 ..  9  typ_code,
              9 .. 10  typ_ec,
@@ -59,8 +59,8 @@ abstract segment SegmentDescriptorBase(base: addr) {
     }
 
     interface(base: addr) {
-        mem entry_lo [ base, 0, 4 ],
-        mem entry_hi [ base, 4, 4 ],
+        mmio entry_lo [ base, 0, 4 ],
+        mmio entry_hi [ base, 4, 4 ],
     }
 
     #[remap]

lib/velosiast/src/ast/interface/fields/mod.rs

@@ -106,6 +106,15 @@ impl VelosiAstInterfaceField {
         }
     }
 
+    pub fn offset(&self) -> u64 {
+        match self {
+            VelosiAstInterfaceField::Memory(field) => field.offset,
+            VelosiAstInterfaceField::Register(_field) => 0,
+            VelosiAstInterfaceField::Mmio(field) => field.offset,
+            VelosiAstInterfaceField::Instruction(_field) => 0,
+        }
+    }
+
     pub fn nbits(&self) -> u64 {
         match self {
             VelosiAstInterfaceField::Memory(field) => field.nbits(),

lib/velosiast/src/ast/interface/mod.rs

@@ -233,6 +233,14 @@ impl VelosiAstInterface {
             .collect::<HashSet<Rc<String>>>()
     }
 
+    pub fn register_region_size(&self) -> u64 {
+        self.fields
+            .iter()
+            .map(|f| f.offset() + f.size())
+            .max()
+            .unwrap_or(0)
+    }
+
     pub fn bit_slice_idents(&self) -> HashSet<Rc<String>> {
         self.fields
             .iter()