Hybrid memory representation #400

danblitzhou · 2021-04-30T14:36:18Z

added OpSemMemHybridRepr: store: array theory, load: ITE
iterative rewrite function for store Expr during loadAlignedWordFromMem for hybrid repr

priyasiddharth

Left some comments mainly for my understanding...

priyasiddharth · 2021-05-01T01:59:10Z

lib/seahorn/BvOpSem2MemRepr.cc

+/**
+ * rewriter for store expr:
+ * e = store A idx val -> { return ite( (idx == ptr), val, rewrite(A) )}
+ * e is not store (const array or terminal register) ->


IIUC changing store to ite will allow us to hit the SAT solver rather than the SMT solver which knows about arrays.

priyasiddharth · 2021-05-01T02:10:53Z

lib/seahorn/BvOpSem2MemRepr.cc

+  Expr doPtrEq(Expr p1, Expr p2) { return m_alu.doEq(p1, p2, m_ptrSz); }
+
+  Expr operator()(Expr e) {
+    if (isOp<STORE>(e)) {


will adding an assert that we expect a struct with three fields help with debugging?

priyasiddharth · 2021-05-01T02:16:43Z

lib/seahorn/BvOpSem2MemRepr.cc

+  LOG("opsem-hybrid", INFO << "From ptr " << *mem.toExpr() << "\n");
+
+  /** rewrite store into ITE **/
+  ArrayStoreRewriter rw(ptr.toExpr(), m_ctx.alu(),


IIUC when we load we lazily rewrite the store instructions in the memory array rather than rewriting everytime we store... is this correct?

yes. optimizing while doing so. next layer is to optimize store instructions to simplify load optimizations later on

agurfinkel · 2021-08-20T14:27:28Z

include/seahorn/Expr/ExprRewriter.hh

+Expr rewriteITEComp(Expr exp);
+
+struct RewriteFrame {
+  Expr m_exp;


comment the role of the fields

agurfinkel · 2021-08-20T14:28:53Z

include/seahorn/Expr/ExprRewriter.hh

+  /* apply rewrite rules */
+protected:
+  ExprFactory &m_efac; // for making expr
+  EZ3 &m_zctx;         // for z3 simplifier if needed


I don't see why generic rewriter should depend on Z3. Its specialization can, but the generic rewriter should not

agurfinkel · 2021-08-20T14:29:49Z

include/seahorn/Expr/ExprRewriter.hh

+protected:
+  Config m_config;
+  ExprFactory &m_efac; // for making expr
+  EZ3 &m_zctx;         // for z3 simplifier if needed


should not be part of generic rewriter

agurfinkel · 2021-08-20T14:32:10Z

include/seahorn/Expr/ExprRewriter.hh

+    in any of the above case, push e to top of result stack
+    otherwise return false and push e into top of rewriteStack
+  */
+  bool visited(Expr e, size_t depth) {


the function has too many side-effects. The name does not reflect them all, neither does the comment.

perhaps renaming the function into visit would go long way to address the comment above

include/seahorn/Expr/ExprRewriter.hh

agurfinkel · 2021-08-20T14:37:05Z

include/seahorn/Expr/ExprRewriter.hh

+    rewrite_result rwRes = m_config.applyRewriteRules(new_exp);
+    if (rwRes.status == rewrite_status::RW_DONE) {
+      m_resultStack.push_back(rwRes.rewritten);
+      if (exp->use_count() > 1) {


replace exp->use_count() > 1 with shouldCache function for readability. Here and elsewhere

agurfinkel · 2021-08-20T14:38:55Z

include/seahorn/Expr/ExprRewriter.hh

+    m_resultStack.resize(begin);
+    // apply rewrite rules to expression with new kids
+    rewrite_result rwRes = m_config.applyRewriteRules(new_exp);
+    if (rwRes.status == rewrite_status::RW_DONE) {


there has to be a way for a rule to indicate that no rewrite has happened. In this case, the result should not be cached.

perhaps add a new status RW_SKIPPED

agurfinkel · 2021-08-20T14:40:20Z

include/seahorn/Expr/ExprVisitor.hh

+/* Pair <mem, ptr> */
+using DagVisitMemCache = std::unordered_map<ENode *, ExprPair>;
+
+inline Expr findInDagVisitCache(DagVisitCache &cache, Expr expr) {


what is this for? Document

not sure if this is needed anymore

agurfinkel · 2021-09-14T13:44:05Z

include/seahorn/Expr/ExprRewriteRule.hh

      }
    }
+    // ite(true, a, b) => a
+    if (isOpX<TRUE>(i)) {
+      return {t, rewrite_status::RW_1};


why RW_1 ? a is already rewritten

agurfinkel · 2021-09-14T13:44:42Z

include/seahorn/Expr/ExprRewriteRule.hh

+    }
+    // ite(false, a, b) => b
+    if (isOpX<FALSE>(i)) {
+      return {e, rewrite_status::RW_1};


agurfinkel · 2021-09-14T13:46:06Z

include/seahorn/Expr/ExprRewriteRule.hh

@@ -151,7 +152,45 @@ struct BoolOpRewriteRule : public ExprRewriteRule {
    if (isOpX<NEG>(exp)) {
      Expr neg = exp->arg(0);
      if (isOpX<NEG>(neg)) {
-        return {neg->arg(0), rewrite_status::RW_2};
+        return {neg->arg(0), rewrite_status::RW_1};


agurfinkel · 2021-09-14T13:49:02Z

include/seahorn/Expr/ExprRewriteRule.hh

+        Expr e = arr->arg(2);
+        Expr new_t = op::array::select(t, idx);
+        Expr new_e = op::array::select(e, idx);
+        return {mk<ITE>(i, new_t, new_e), rewrite_status::RW_2};


overall, this is potentially very expensive in our application. It will create a lot of intermediate expressions while select is being pushed down. It would be more effective to implement push_select_over_ite method that pushes select to the bottom of the ite tree in one operation.

agurfinkel · 2021-09-14T13:50:19Z

include/seahorn/Expr/ExprRewriteRule.hh

+      /** Read-over-write: select(store(arr_w, idx_w, val), idx_r)
+          ==> ite(idx_w == idx_x, val, select(arr_w, idx_r))
+       **/
+      if (isOpX<STORE>(arr)) {


same comment as above. Need a single operation that pushes select down a chain of stores, and maybe a combination that pushes select through the chain of ite and store

LinerSu · 2022-02-14T22:03:00Z

lib/seahorn/Smt/ExprAddrRangeMap.cc

+}
+
+AddrRange zeroBitsRange(AddrRange &r, size_t bits) {
+  unsigned new_low = r.low >> bits;


This should check or assume r.isTop == false at first.

good catch so that we can skip some operations

LinerSu · 2022-02-15T01:53:51Z

lib/seahorn/Smt/ExprRewriter.cc

+}
+} // namespace utils
+
+Expr rewriteHybridLoadMemExpr(Expr loadMem, Expr ptr, AddrRangeMap &arm) {


I am confused about parameters you passed for this method. Why you add ptr but not use it?

LinerSu · 2022-02-15T02:04:19Z

include/seahorn/Expr/ExprRewriter.hh

+  ITECompRewriteConfig(ExprFactory &efac, DagVisitCache &cache,
+                       AddrRangeMap &arm)
+      : m_iteRule(efac, cache), m_compRule(efac, cache),
+        m_boolRule(efac, cache), m_arrayRule(efac, cache, arm),


Looks like you only use ARM for select only. Maybe I did not fully get the usage of the ARM. Can Arm be used for other pointer expressions?

we can perhaps use it during the initial rewrite from stores to ITEs

(to sqaush): use rewriter to apply pattern recursively feat(ExprVisitor): set selected kids to visit instead of always visit all (tsquash): use more restrained vistor to only visit first arg of store (tsquash): rename, cleanup use simple custom rewriter for array store; revert m_selectedKids

in house version is gud feat(mem-repr): iterative rewriter for ITE expr

(intrim): cached visit; stateless rules (intrim): OOP design

draft(nmr): present stack ptr expr with based obj type draft(nmr): low precision but sound addr filtering draft(hybrid): push down bvadd; better addrs range draft(hybrid): AddrRange data struc to keep track of isTop

agurfinkel · 2022-12-09T20:15:00Z

@danblitzhou can we close this PR?

danblitzhou · 2022-12-09T23:24:27Z

Yes, the new PR should replace this one. Arie Gurfinkel ***@***.***>于2022年12月9日周五下午3:15写道：

…

@danblitzhou <https://github.com/danblitzhou> can we close this PR? — Reply to this email directly, view it on GitHub <#400 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AEHINGS3NR7HTQ6AZNP2KZ3WMOHM5ANCNFSM434L376A> . You are receiving this because you were mentioned.Message ID: ***@***.***>

danblitzhou requested a review from agurfinkel April 30, 2021 14:36

priyasiddharth reviewed May 1, 2021

View reviewed changes

danblitzhou force-pushed the new-mem-repr branch from 6a0fddc to 61e489f Compare June 17, 2021 03:34

danblitzhou force-pushed the new-mem-repr branch 2 times, most recently from d726b99 to 716e1ac Compare July 16, 2021 07:23

danblitzhou force-pushed the new-mem-repr branch from 6d8770b to 2d51832 Compare July 23, 2021 12:56

danblitzhou force-pushed the new-mem-repr branch from 2d51832 to 9344400 Compare August 6, 2021 04:15

agurfinkel requested changes Aug 20, 2021

View reviewed changes

danblitzhou force-pushed the new-mem-repr branch 2 times, most recently from 2a23a0d to ac0b752 Compare August 27, 2021 05:32

danblitzhou force-pushed the new-mem-repr branch from 853ce4e to 7eea7fc Compare September 14, 2021 04:44

agurfinkel reviewed Sep 14, 2021

View reviewed changes

danblitzhou force-pushed the new-mem-repr branch 2 times, most recently from 8d1d06e to 4dc0a6c Compare October 6, 2021 04:43

danblitzhou force-pushed the new-mem-repr branch from 4dc0a6c to 55d832c Compare February 9, 2022 21:30

LinerSu reviewed Feb 15, 2022

View reviewed changes

danblitzhou force-pushed the new-mem-repr branch from 54af027 to 41be486 Compare March 2, 2022 02:39

danblitzhou added 9 commits May 12, 2022 16:21

test(mem-repr): add hybrid repr tests to opsem

334ef61

feat(mem-repr): use iterative pattern for array-store rewritter

6d1b260

feat(mem-repr): add simple ite simplifier together with z3 simp

20c15aa

feat(mem-repr): properly implement cross load caching

7ecfe2f

feat(mem-repr): iterative rewriter for ITE expr

1cfb354

in house version is gud feat(mem-repr): iterative rewriter for ITE expr

feat(mem-repr): refactored generic rewriter with multi-lvl revisit

e00e31a

(intrim): cached visit; stateless rules (intrim): OOP design

feat(mem-repr): revamp into z3-like rewriter algo with result stack

57dc9a3

feat(mem-repr): remove z3 ctx from base rule; smaller optmztns

5d24e9b

danblitzhou added 11 commits May 12, 2022 16:29

feat(mem-repr): skip out of range stores

582da9c

draft(nmr): present stack ptr expr with based obj type draft(nmr): low precision but sound addr filtering draft(hybrid): push down bvadd; better addrs range draft(hybrid): AddrRange data struc to keep track of isTop

feat(mem-repr): AddrRangeMap for over-approx ptr access range

8c8c8c4

feat(mem-repr): handle pointer alignment

19766ac

feat(mem-repr): use zero bits semantics

f79dac0

feat(mem-repr): rw value read from written mem

d4a6332

feat(mem-repr): cache during ARM building

0ecbf55

feat(memrepr): memset memcpy

dfb486a

fix(memRepr): do not rely on ARM for memset/cpy

cc11b43

feat(memRepr): memwords op Expr

0db758a

feat(memRepr): caching during RW; skip simp

18ae177

feat(memRepr): use z3 simplification for hybrid

32dc446

danblitzhou force-pushed the new-mem-repr branch from 2ac3778 to d67474b Compare May 12, 2022 20:33

feat(memRepr): use rewriter to push select down

2aaa1a4

danblitzhou force-pushed the new-mem-repr branch from d67474b to 2aaa1a4 Compare May 12, 2022 20:41

feat(memRepr): revert recursive createWord for test

25d8b15

danblitzhou force-pushed the new-mem-repr branch from fcaa854 to 25d8b15 Compare May 25, 2022 19:37

danblitzhou added 7 commits May 26, 2022 00:13

feat(memRepr): cache multi-step rewrites

c33bd89

feat(memRepr): AddrRange and ARM abstractions

12e4701

feat(memRepr): store map impl

442f34f

feat(memRepr): store map tests

a9c32b0

feat(memrepr): use rewriter to handle all compares

e284e2b

feat(memrepr): properly handle references count of Expr in generic cache

ca08a7d

feat(memrepr): count number of read-over-writes

d1e76bd

danblitzhou force-pushed the new-mem-repr branch from 966c04f to af1b26b Compare October 11, 2022 19:51

feat(memrepr): store-map rework for log insertion

a3b486f

danblitzhou force-pushed the new-mem-repr branch from af1b26b to a3b486f Compare October 11, 2022 21:06

feat(smt): add marshaling for UADD_NO_OVERFLOW for yices2

b670350

danblitzhou mentioned this pull request Nov 29, 2022

SeaM implementation #473

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Hybrid memory representation #400

Hybrid memory representation #400

danblitzhou commented Apr 30, 2021

priyasiddharth left a comment

priyasiddharth May 1, 2021

priyasiddharth May 1, 2021

priyasiddharth May 1, 2021

agurfinkel May 1, 2021

agurfinkel Aug 20, 2021

agurfinkel Aug 20, 2021

agurfinkel Aug 20, 2021

agurfinkel Aug 20, 2021

agurfinkel Aug 20, 2021

agurfinkel Aug 20, 2021

agurfinkel Aug 20, 2021

danblitzhou Aug 20, 2021

agurfinkel Aug 20, 2021

agurfinkel Aug 20, 2021

danblitzhou Aug 20, 2021

agurfinkel Sep 14, 2021

agurfinkel Sep 14, 2021

agurfinkel Sep 14, 2021

agurfinkel Sep 14, 2021

agurfinkel Sep 14, 2021

LinerSu Feb 14, 2022

danblitzhou Feb 15, 2022

LinerSu Feb 15, 2022

danblitzhou Feb 15, 2022

LinerSu Feb 15, 2022

danblitzhou Feb 15, 2022

agurfinkel commented Dec 9, 2022

danblitzhou commented Dec 9, 2022 via email

Hybrid memory representation #400

Are you sure you want to change the base?

Hybrid memory representation #400

Conversation

danblitzhou commented Apr 30, 2021

priyasiddharth left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

agurfinkel commented Dec 9, 2022

danblitzhou commented Dec 9, 2022 via email