Skip to content

Commit

Permalink
Implement several common python AST methods (#11)
Browse files Browse the repository at this point in the history
* Implement several common python AST methods

* Cargo fmt
  • Loading branch information
twizmwazin authored Oct 31, 2024
1 parent 770cac8 commit b706d9b
Show file tree
Hide file tree
Showing 19 changed files with 691 additions and 134 deletions.
5 changes: 2 additions & 3 deletions crates/clarirs_core/src/algorithms/simplify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,8 @@ impl<'c> Simplify<'c> for BitVecAst<'c> {
BitVecOp::URem(arc, arc1) => todo!(),
BitVecOp::SRem(arc, arc1) => todo!(),
BitVecOp::Pow(arc, arc1) => todo!(),
BitVecOp::LShL(arc, arc1) => todo!(),
BitVecOp::ShL(arc, arc1) => todo!(),
BitVecOp::LShR(arc, arc1) => todo!(),
BitVecOp::AShL(arc, arc1) => todo!(),
BitVecOp::AShR(arc, arc1) => todo!(),
BitVecOp::RotateLeft(arc, arc1) => todo!(),
BitVecOp::RotateRight(arc, arc1) => todo!(),
Expand Down Expand Up @@ -129,7 +128,7 @@ impl<'c> Simplify<'c> for StringAst<'c> {
.context()
.simplification_cache
.get_or_insert_with_string(self.hash(), || match &self.op() {
StringOp::StringS(_, _) => todo!(),
StringOp::StringS(_) => todo!(),
StringOp::StringV(_) => todo!(),
StringOp::StrConcat(arc, arc1) => todo!(),
StringOp::StrSubstr(arc, arc1, arc2) => todo!(),
Expand Down
40 changes: 20 additions & 20 deletions crates/clarirs_core/src/algorithms/tests/test_bv.rs
Original file line number Diff line number Diff line change
Expand Up @@ -341,59 +341,59 @@ fn test_not() -> Result<()> {
}

#[test]
fn test_lshr() -> Result<()> {
fn test_shl() -> Result<()> {
let ctx = Context::new();

let table: Vec<(u64, u64, u64)> = vec![
(0, 0, 0),
(0, 1, 0),
(1, 0, 1),
(1, 1, 0),
(1, 2, 0),
(2, 1, 1),
(2, 2, 0),
(2, 3, 0),
(3, 2, 0),
(3, 3, 0),
(1, 1, 2),
(1, 2, 4),
(2, 1, 4),
(2, 2, 8),
(2, 3, 16),
(3, 2, 12),
(3, 3, 24),
(u64::MAX, 1, u64::MAX),
(u64::MAX, 2, u64::MAX),
];

for (a, b, expected) in table {
let a = ctx.bvv_prim(a).unwrap();
let b = ctx.bvv_prim(b).unwrap();
let expected = ctx.bvv_prim(expected).unwrap();

let result = ctx.lshr(&a, &b)?.simplify()?;
let result = ctx.shl(&a, &b)?.simplify()?;
assert_eq!(result, expected);
}

Ok(())
}

#[test]
fn test_ashl() -> Result<()> {
fn test_lshr() -> Result<()> {
let ctx = Context::new();

let table: Vec<(u64, u64, u64)> = vec![
(0, 0, 0),
(0, 1, 0),
(1, 0, 1),
(1, 1, 2),
(1, 2, 4),
(2, 1, 4),
(2, 2, 8),
(2, 3, 16),
(3, 2, 12),
(3, 3, 24),
(u64::MAX, 1, u64::MAX),
(u64::MAX, 2, u64::MAX),
(1, 1, 0),
(1, 2, 0),
(2, 1, 1),
(2, 2, 0),
(2, 3, 0),
(3, 2, 0),
(3, 3, 0),
];

for (a, b, expected) in table {
let a = ctx.bvv_prim(a).unwrap();
let b = ctx.bvv_prim(b).unwrap();
let expected = ctx.bvv_prim(expected).unwrap();

let result = ctx.ashl(&a, &b)?.simplify()?;
let result = ctx.lshr(&a, &b)?.simplify()?;
assert_eq!(result, expected);
}

Expand Down
8 changes: 3 additions & 5 deletions crates/clarirs_core/src/ast/bitvec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,8 @@ pub enum BitVecOp<'c> {
URem(BitVecAst<'c>, BitVecAst<'c>),
SRem(BitVecAst<'c>, BitVecAst<'c>),
Pow(BitVecAst<'c>, BitVecAst<'c>),
LShL(BitVecAst<'c>, BitVecAst<'c>),
ShL(BitVecAst<'c>, BitVecAst<'c>),
LShR(BitVecAst<'c>, BitVecAst<'c>),
AShL(BitVecAst<'c>, BitVecAst<'c>),
AShR(BitVecAst<'c>, BitVecAst<'c>),
RotateLeft(BitVecAst<'c>, BitVecAst<'c>),
RotateRight(BitVecAst<'c>, BitVecAst<'c>),
Expand All @@ -36,7 +35,7 @@ pub enum BitVecOp<'c> {
FpToIEEEBV(FloatAst<'c>),
FpToUBV(FloatAst<'c>, u32, FPRM),
FpToSBV(FloatAst<'c>, u32, FPRM),
StrLen(StringAst<'c>), // or StrLen(BitVecAst<'c>, u32),
StrLen(StringAst<'c>),
StrIndexOf(StringAst<'c>, StringAst<'c>, BitVecAst<'c>),
StrToBV(StringAst<'c>),
If(AstRef<'c, BooleanOp<'c>>, BitVecAst<'c>, BitVecAst<'c>),
Expand Down Expand Up @@ -72,9 +71,8 @@ impl<'c> Op<'c> for BitVecOp<'c> {
| BitVecOp::URem(a, b)
| BitVecOp::SRem(a, b)
| BitVecOp::Pow(a, b)
| BitVecOp::LShL(a, b)
| BitVecOp::ShL(a, b)
| BitVecOp::LShR(a, b)
| BitVecOp::AShL(a, b)
| BitVecOp::AShR(a, b)
| BitVecOp::RotateLeft(a, b)
| BitVecOp::RotateRight(a, b)
Expand Down
12 changes: 4 additions & 8 deletions crates/clarirs_core/src/ast/factory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,12 +41,8 @@ pub trait AstFactory<'c>: Sized {
self.make_float(FloatOp::FPV(value.into()))
}

fn strings<S: Into<String>>(
&'c self,
name: S,
width: u32,
) -> Result<StringAst<'c>, ClarirsError> {
self.make_string(StringOp::StringS(name.into(), width))
fn strings<S: Into<String>>(&'c self, name: S) -> Result<StringAst<'c>, ClarirsError> {
self.make_string(StringOp::StringS(name.into()))
}

fn stringv<S: Into<String>>(&'c self, value: S) -> Result<StringAst<'c>, ClarirsError> {
Expand Down Expand Up @@ -164,12 +160,12 @@ pub trait AstFactory<'c>: Sized {
Op::pow(self, lhs, rhs)
}

fn ashl(
fn shl(
&'c self,
lhs: &BitVecAst<'c>,
rhs: &BitVecAst<'c>,
) -> Result<BitVecAst<'c>, ClarirsError> {
self.make_bitvec(BitVecOp::AShL(lhs.clone(), rhs.clone()))
self.make_bitvec(BitVecOp::ShL(lhs.clone(), rhs.clone()))
}

fn ashr(
Expand Down
7 changes: 7 additions & 0 deletions crates/clarirs_core/src/ast/node.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ pub struct AstNode<'c, O: Op<'c>> {
symbolic: bool,
#[serde(skip)]
variables: HashSet<String>,
#[serde(skip)]
depth: u32,
}

impl<'c, O> Debug for AstNode<'c, O>
Expand Down Expand Up @@ -73,6 +75,7 @@ impl<'c, O: Op<'c> + Serialize> AstNode<'c, O> {
hash,
symbolic,
variables,
depth: 0, // TODO: Implement depth calculation
}
}

Expand All @@ -91,6 +94,10 @@ impl<'c, O: Op<'c> + Serialize> AstNode<'c, O> {
pub fn variables(&self) -> &HashSet<String> {
&self.variables
}

pub fn depth(&self) -> u32 {
self.depth
}
}

impl<'c, O: Op<'c>> Op<'c> for AstNode<'c, O> {
Expand Down
4 changes: 2 additions & 2 deletions crates/clarirs_core/src/ast/string.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use crate::prelude::*;

#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize)]
pub enum StringOp<'c> {
StringS(String, u32),
StringS(String),
StringV(String),
StrConcat(StringAst<'c>, StringAst<'c>),
StrSubstr(StringAst<'c>, BitVecAst<'c>, BitVecAst<'c>),
Expand Down Expand Up @@ -38,7 +38,7 @@ impl<'c> Op<'c> for StringOp<'c> {
}

fn variables(&self) -> HashSet<String> {
if let StringOp::StringS(s, _) = self {
if let StringOp::StringS(s) = self {
let mut set = HashSet::new();
set.insert(s.clone());
set
Expand Down
12 changes: 11 additions & 1 deletion crates/clarirs_num/src/bitvec.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use std::fmt::Debug;
use std::ops::{Add, BitAnd, BitOr, BitXor, Div, Mul, Neg, Not, Rem, Shl, Shr, Sub};

use num_bigint::BigUint;
use num_bigint::{BigInt, BigUint};

Check warning on line 4 in crates/clarirs_num/src/bitvec.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest

unused import: `BigInt`

Check warning on line 4 in crates/clarirs_num/src/bitvec.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest

unused import: `BigInt`

Check warning on line 4 in crates/clarirs_num/src/bitvec.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest

unused import: `BigInt`

Check warning on line 4 in crates/clarirs_num/src/bitvec.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest

unused import: `BigInt`

Check warning on line 4 in crates/clarirs_num/src/bitvec.rs

View workflow job for this annotation

GitHub Actions / cargo clippy

unused import: `BigInt`

Check warning on line 4 in crates/clarirs_num/src/bitvec.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest

unused import: `BigInt`

Check warning on line 4 in crates/clarirs_num/src/bitvec.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest

unused import: `BigInt`
use serde::{Deserialize, Serialize};
use smallvec::SmallVec;
use thiserror::Error;
Expand Down Expand Up @@ -72,6 +72,16 @@ impl BitVec {
)
}

pub fn as_biguint(&self) -> BigUint {
BigUint::from_bytes_be(
self.words
.iter()
.flat_map(|w| w.to_be_bytes())
.collect::<Vec<u8>>()
.as_slice(),
)
}

pub fn sign(&self) -> bool {
return self
.words
Expand Down
8 changes: 8 additions & 0 deletions crates/clarirs_num/src/float.rs
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,14 @@ impl Float {

Self::new(self.sign, exponent, mantissa)
}

pub fn as_f64(&self) -> f64 {
recompose_f64(
self.sign as u8,
*self.exponent.as_biguint().to_u64_digits().first().unwrap() as u16,
*self.mantissa.as_biguint().to_u64_digits().first().unwrap(),
)
}
}

impl From<f32> for Float {
Expand Down
Loading

0 comments on commit b706d9b

Please sign in to comment.