Testcase gen (#15)

* auto gen * add logic to repeat simulation of a file --------- Co-authored-by: Sanjit Basker <tijnasreksab@gmail.com>
NgaiJustin · Dec 11, 2023 · 54bc548 · 54bc548
1 parent 5707538
commit 54bc548
Show file tree

Hide file tree

Showing 5 changed files with 195 additions and 34 deletions.
diff --git a/src/cli.rs b/src/cli.rs
@@ -8,6 +8,14 @@ pub struct CLI {
   #[arg(short, long, action)]
   pub file: Option<String>,
 
+  /// Profile mode
+  #[arg(short, long, default_value = "false")]
+  pub profile: bool,
+
+  /// The number of times to repeat the simulation (used for profiling)
+  #[arg(short, long, default_value = "1")]
+  pub num_repeat: usize,
+
   /// Inputs for the main function
   #[arg(action)]
   pub inputs: Vec<String>,

diff --git a/src/main.rs b/src/main.rs
@@ -12,6 +12,7 @@ use tempfile::NamedTempFile;
 fn main() -> InterpResult<()> {
   let start = Instant::now();
   let args = cli::CLI::parse();
+  println!("{:?}", args.num_repeat);
 
   let btor2_file = match args.file {
     None => {
@@ -27,47 +28,51 @@ fn main() -> InterpResult<()> {
   let mut parser = Btor2Parser::new();
   let btor2_lines = parser.read_lines(&btor2_file).unwrap().collect::<Vec<_>>();
 
-  // Collect node sorts
-  let node_sorts = btor2_lines
-    .iter()
-    .map(|line| match line.tag() {
-      btor2tools::Btor2Tag::Sort | btor2tools::Btor2Tag::Output => 0,
-      _ => match line.sort().content() {
-        btor2tools::Btor2SortContent::Bitvec { width } => usize::try_from(width).unwrap(),
-        btor2tools::Btor2SortContent::Array { .. } => 0, // TODO: handle arrays
-      },
-    })
-    .collect::<Vec<_>>();
+  for _ in 0..args.num_repeat {
+    // Collect node sorts
+    let node_sorts = btor2_lines
+      .iter()
+      .map(|line| match line.tag() {
+        btor2tools::Btor2Tag::Sort | btor2tools::Btor2Tag::Output => 0,
+        _ => match line.sort().content() {
+          btor2tools::Btor2SortContent::Bitvec { width } => usize::try_from(width).unwrap(),
+          btor2tools::Btor2SortContent::Array { .. } => 0, // TODO: handle arrays
+        },
+      })
+      .collect::<Vec<_>>();
 
-  // Init environment
-  // let mut env = interp::Environment::new(btor2_lines.len() + 1);
-  let mut s_env = shared_env::SharedEnvironment::new(node_sorts);
+    // Init environment
+    // let mut env = interp::Environment::new(btor2_lines.len() + 1);
+    let mut s_env = shared_env::SharedEnvironment::new(node_sorts);
 
-  // Parse inputs
-  match interp::parse_inputs(&mut s_env, &btor2_lines, &args.inputs) {
-    Ok(()) => {}
-    Err(e) => {
-      eprintln!("{}", e);
-      std::process::exit(1);
-    }
-  };
+    // Parse inputs
+    match interp::parse_inputs(&mut s_env, &btor2_lines, &args.inputs) {
+      Ok(()) => {}
+      Err(e) => {
+        eprintln!("{}", e);
+        std::process::exit(1);
+      }
+    };
 
-  // Main interpreter loop
-  interp::interpret(btor2_lines.iter(), &mut s_env)?;
+    // Main interpreter loop
+    interp::interpret(btor2_lines.iter(), &mut s_env)?;
 
-  // // Print result of execution
-  println!("{}", s_env);
+    // Print result of execution
+    if !args.profile {
+      println!("{}", s_env);
 
-  // Extract outputs
-  btor2_lines.iter().for_each(|line| {
-    if let btor2tools::Btor2Tag::Output = line.tag() {
-      let output_name = line.symbol().unwrap().to_string_lossy().into_owned();
-      let src_node_idx = line.args()[0] as usize;
-      let output_val = s_env.get(src_node_idx);
+      // Extract outputs
+      btor2_lines.iter().for_each(|line| {
+        if let btor2tools::Btor2Tag::Output = line.tag() {
+          let output_name = line.symbol().unwrap().to_string_lossy().into_owned();
+          let src_node_idx = line.args()[0] as usize;
+          let output_val = s_env.get(src_node_idx);
 
-      println!("{}: {}", output_name, output_val);
+          println!("{}: {}", output_name, output_val);
+        }
+      });
     }
-  });
+  }
 
   // print to stderr the time it took to run
   let duration = start.elapsed();

diff --git a/test/auto-testcases/gen_inputs.py b/test/auto-testcases/gen_inputs.py
@@ -0,0 +1,5 @@
+import random
+
+inputs = [f'input{i}' for i in range(8)]
+vals = [f'0b{"".join(str(random.randint(0, 1)) for _ in range(32))}' for i in range(8)]
+print(' '.join(f'{a}={b}' for a, b in zip(inputs, vals)))
diff --git a/test/auto-testcases/gen_xor_cat.btor2 b/test/auto-testcases/gen_xor_cat.btor2
@@ -0,0 +1,78 @@
+; cargo run -r -- -f gen_xor_cat.btor2
+; many XORs followed by splitting the output into chunks
+1 sort bitvec 32
+2 sort bitvec 64
+3 sort bitvec 128
+4 sort bitvec 256
+5 sort bitvec 512
+6 input 1 input0
+7 input 1 input1
+8 input 1 input2
+9 input 1 input3
+10 input 1 input4
+11 input 1 input5
+12 input 1 input6
+13 input 1 input7
+14 xor 1 8 12
+15 xor 1 7 6
+16 xor 1 12 10
+17 xor 1 13 6
+18 xor 1 10 6
+19 xor 1 9 11
+20 xor 1 8 6
+21 xor 1 12 7
+22 xor 1 10 9
+23 xor 1 8 13
+24 xor 1 9 12
+25 xor 1 12 13
+26 xor 1 13 12
+27 xor 1 7 6
+28 xor 1 9 8
+29 xor 1 8 6
+30 xor 1 28 18
+31 xor 1 15 23
+32 xor 1 29 22
+33 xor 1 27 28
+34 xor 1 24 27
+35 xor 1 14 26
+36 xor 1 19 29
+37 xor 1 19 24
+38 xor 1 24 24
+39 xor 1 23 20
+40 xor 1 17 18
+41 xor 1 18 22
+42 xor 1 23 25
+43 xor 1 20 28
+44 xor 1 27 16
+45 xor 1 26 26
+46 concat 2 30 31
+47 concat 2 32 33
+48 concat 2 34 35
+49 concat 2 36 37
+50 concat 2 38 39
+51 concat 2 40 41
+52 concat 2 42 43
+53 concat 2 44 45
+54 concat 3 46 47
+55 concat 3 48 49
+56 concat 3 50 51
+57 concat 3 52 53
+58 concat 4 54 55
+59 concat 4 56 57
+60 concat 5 58 59
+61 slice 1 60 31 0
+62 slice 1 60 63 32
+63 slice 1 60 95 64
+64 slice 1 60 127 96
+65 slice 1 60 159 128
+66 slice 1 60 191 160
+67 slice 1 60 223 192
+68 slice 1 60 255 224
+69 output 61 output0
+70 output 62 output1
+71 output 63 output2
+72 output 64 output3
+73 output 65 output4
+74 output 66 output5
+75 output 67 output6
+76 output 68 output7
diff --git a/test/auto-testcases/gen_xor_city.py b/test/auto-testcases/gen_xor_city.py
@@ -0,0 +1,65 @@
+from random import randint
+
+"""; BTOR description generated by Yosys 0.33+65 (git sha1 90124dce5, clang 15.0.0 -fPIC -Os) for module std_neq.
+; ARGS: left=54321 right=12345
+1 sort bitvec 32
+2 input 1 left ; core.sv:167.34-167.38
+3 input 1 right ; core.sv:168.34-168.39
+4 sort bitvec 1
+5 neq 4 2 3
+6 output 5 out ; core.sv:169.18-169.21
+; end of yosys output"""
+
+if __name__ == '__main__':
+    starting_lines = [
+        '; many XORs followed by splitting the output into chunks'
+    ] + [f'{i} sort bitvec {16 * (2 ** i)}' for i in range(1, 6)]
+
+    arg_lines = []
+    for node_id in range(6, 14):
+        arg_lines.append(f'{node_id} input 1 input{node_id - 6}')
+
+    xor_lines = []
+    for node_id in range(14, 30):
+        xor_lines.append(f'{node_id} xor 1 {randint(6, 13)} {randint(6, 13)}')
+
+    double_xor_lines = []
+    for node_id in range(30, 46):
+        double_xor_lines.append(f'{node_id} xor 1 {randint(14, 29)} {randint(14, 29)}')
+
+    concat_lines = []
+    for node_id in range(46, 54):
+        first = 30 + 2 * (node_id - 46)
+        second = first + 1
+        concat_lines.append(f'{node_id} concat 2 {first} {second}')
+
+    for node_id in range(54, 58):
+        first = 46 + 2 * (node_id - 54)
+        second = first + 1
+        concat_lines.append(f'{node_id} concat 3 {first} {second}')
+
+    for node_id in range(58, 60):
+        first = 54 + 2 * (node_id - 58)
+        second = first + 1
+        concat_lines.append(f'{node_id} concat 4 {first} {second}')
+
+    concat_lines.append('60 concat 5 58 59')
+
+    output_lines = []
+    curr_node_id = 61
+    curr_pos = 0
+    for i in range(2 ** 3):
+        output_lines.append(f'{curr_node_id} slice 1 60 {curr_pos + 31} {curr_pos}')
+        curr_pos += 32
+        curr_node_id += 1
+
+    for i in range(2 ** 3):
+        output_lines.append(f'{curr_node_id} output {curr_node_id - 8} output{i}')
+        curr_node_id += 1
+
+    print("\n".join(starting_lines))
+    print("\n".join(arg_lines))
+    print("\n".join(xor_lines))
+    print("\n".join(double_xor_lines))
+    print("\n".join(concat_lines))
+    print("\n".join(output_lines))