32bit support (#64)

* First line of 64bit support, try to use inline ifs Major changes builder.rs * Finished with 32bit, cosmetic need to be done * most ifs removed, composition with struct * fixed bug with the memory writing * 32bit overflow bad state added, some polishings needs to be done * added 32 bit flag * 32bit flag bug fixes, to small memory * Overflow check redone * Overflow check redone --------- Co-authored-by: Patrick Weber <[email protected]>
cksystemsgroup · Apr 17, 2024 · 1d77ed2 · 1d77ed2
1 parent c977be2
commit 1d77ed2
Show file tree

Hide file tree

Showing 12 changed files with 411 additions and 69 deletions.
diff --git a/examples/addOverflow.c b/examples/addOverflow.c
@@ -0,0 +1,16 @@
+uint64_t main() {
+    uint64_t  a;
+    uint64_t* x;
+
+    a = 2147483647;
+
+    x = malloc(8);
+
+    *x = 0;
+
+    read(0, x, 1);
+
+    a = a + *x;
+
+    return 0;
+}
diff --git a/examples/mulOverflow.c b/examples/mulOverflow.c
@@ -0,0 +1,17 @@
+uint64_t main() {
+    uint64_t  a;
+    uint64_t* x;
+    uint64_t y;
+
+    a = 2147483647;
+
+    x = malloc(8);
+
+    *x = 0;
+
+    read(0, x, 1);
+
+    a = a * *x;
+
+    return 0;
+}
diff --git a/examples/negative.c b/examples/negative.c
@@ -0,0 +1,40 @@
+// printing the negative decimal number -7 in C*
+
+// libcstar procedures for printing
+void init_library();
+void print(uint64_t* s);
+void print_integer(uint64_t n);
+void print_hexadecimal(uint64_t n, uint64_t a);
+void print_octal(uint64_t n, uint64_t a);
+void print_binary(uint64_t n, uint64_t a);
+void println();
+
+uint64_t main() {
+  // initialize selfie's libcstar library
+  init_library();
+
+  // print the integer literal -7 in decimal
+  print("-7 in decimal:     ");
+  print_integer(-7);
+  print(" (as signed 64-bit integer)\n");
+
+  // print the integer literal -7 in decimal
+  print("-7 in decimal:     ");
+  print_unsigned_integer(-7);
+  print(" (as unsigned integer)\n");
+
+  // print the integer literal -7 in hexadecimal
+  print("-7 in hexadecimal: ");
+  print_hexadecimal(-7, 0);
+  println();
+
+  // print the integer literal -7 in octal
+  print("-7 in octal:       ");
+  print_octal(-7, 0);
+  println();
+
+  // print the integer literal -7 in binary
+  print("-7 in binary:      ");
+  print_binary(-7, 0);
+  println();
+}
diff --git a/examples/subOverflow.c b/examples/subOverflow.c
@@ -0,0 +1,16 @@
+uint64_t main() {
+    uint64_t  a;
+    uint64_t* x;
+
+    a = -2147483645;
+
+    x = malloc(8);
+
+    *x = 0;
+
+    read(0, x, 1);
+
+    a = a - *x;
+
+    return a;
+}
diff --git a/src/cli.rs b/src/cli.rs
@@ -251,6 +251,12 @@ pub fn args() -> Command {
                         .long("from-btor2")
                         .num_args(0)
                 )
+                .arg(
+                Arg::new("32-bit")
+                    .help("Run beator with an 32 bit version of the Program")
+                    .long("32bit")
+                    .num_args(0)
+                )
                 .arg(
                     Arg::new("extras")
                         .help("Arguments passed to emulated program")

diff --git a/src/engine/system.rs b/src/engine/system.rs
@@ -43,3 +43,28 @@ pub fn prepare_unix_stack(argv: &[String], sp: u64) -> Vec<u64> {
     stack.push(argc);
     stack
 }
+
+pub fn prepare_unix_stack32bit(argv: &[String], sp: u32) -> Vec<u64> {
+    let mut stack32 = vec![];
+    let argc32 = argv.len() as u32;
+    let argv_ptrs32: Vec<u32> = argv
+        .iter()
+        .rev()
+        .map(|arg| {
+            let c_string = arg.to_owned() + "\0";
+            for chunk in c_string.as_bytes().chunks_exact(size_of::<u32>()).rev() {
+                stack32.push(LittleEndian::read_u32(chunk));
+            }
+            sp - (stack32.len() * size_of::<u32>()) as u32
+        })
+        .collect();
+    stack32.push(0); // terminate env table
+    stack32.push(0); // terminate argv table
+    for argv_ptr in argv_ptrs32 {
+        stack32.push(argv_ptr);
+    }
+    // Casting the 32 bit values to 64bit
+    stack32.push(argc32);
+    let stack: Vec<u64> = stack32.iter().map(|&x| x as u64).collect();
+    stack
+}
diff --git a/src/guinea/cli2gui.rs b/src/guinea/cli2gui.rs
@@ -180,7 +180,7 @@ fn output_handling(ui: &mut Ui, data: &mut Guineacorn) {
 
 fn stringify_model(model: &Model) -> String {
     let mut buf = BufWriter::new(Vec::new());
-    let _ = write_model(model, &mut buf);
+    let _ = write_model(model, &mut buf, true);
     let bytes = buf.into_inner().unwrap();
     String::from_utf8(bytes).unwrap()
 }

diff --git a/src/guinea/components/general.rs b/src/guinea/components/general.rs
@@ -47,6 +47,7 @@ pub(crate) fn load(
                 ByteSize::mib(1).as_u64(),
                 8,
                 32,
+                false,
                 &argv,
             )
             .unwrap();

diff --git a/src/main.rs b/src/main.rs
@@ -45,6 +45,9 @@ fn main() -> Result<()> {
     // process global flags
     let log_level = expect_arg::<LogLevel>(&matches, "verbose")?;
 
+    // global bool is64_bit
+    let mut is64_bit = true;
+
     init_logger(log_level)?;
 
     // process subcommands
@@ -94,11 +97,21 @@ fn main() -> Result<()> {
             let arg0 = expect_arg::<String>(args, "input-file")?;
             let extras = collect_arg_values(args, "extras");
 
+            let flag_32bit = args.get_flag("32-bit");
+
             let mut model = if !input_is_dimacs {
                 let mut model = if !input_is_btor2 {
                     let program = load_object_file(&input)?;
+                    is64_bit = program.is64;
                     let argv = [vec![arg0], extras].concat();
-                    generate_model(&program, memory_size, max_heap, max_stack, &argv)?
+                    generate_model(
+                        &program,
+                        memory_size,
+                        max_heap,
+                        max_stack,
+                        flag_32bit,
+                        &argv,
+                    )?
                 } else {
                     parse_btor2_file(&input)
                 };
@@ -223,10 +236,10 @@ fn main() -> Result<()> {
                         }
                     }
                 } else if output_to_stdout {
-                    write_model(&model.unwrap(), stdout())?;
+                    write_model(&model.unwrap(), stdout(), is64_bit)?;
                 } else if let Some(ref output_path) = output {
                     let file = File::create(output_path)?;
-                    write_model(&model.unwrap(), file)?;
+                    write_model(&model.unwrap(), file, is64_bit)?;
                 }
             } else {
                 let is_ising = args.get_flag("ising");

diff --git a/src/unicorn/btor2file_parser.rs b/src/unicorn/btor2file_parser.rs
@@ -147,7 +147,7 @@ impl BTOR2Parser {
         let line = self.lines.get(&nid).unwrap().clone();
         if line[2] == "bitvec" {
             if let Ok(answer) = line[3].parse::<usize>() {
-                return get_nodetype(answer);
+                return get_nodetype(answer, true);
             }
             panic!("Unsupported bitvec: {:?}", line);
         } else if line[2] == "array" {
@@ -313,7 +313,7 @@ impl BTOR2Parser {
                         let bits_src = bits_dest - bits_ext;
                         current_node = Some(NodeRef::from(Node::Ext {
                             nid,
-                            from: get_nodetype(bits_src),
+                            from: get_nodetype(bits_src, true),
                             value,
                         }))
                     }