philzook

10 ms·

61.
by philzook 3y ago
There are some nice coursera courses on minizinc - https://www.coursera.org/learn/discrete-optimization good hats. very fun. - https://www.coursera.org/learn/basic-modeling
62.
by philzook 3y ago
Thanks! Big fan of your posts! Keep it up!
63.
by philzook 3y ago
I do like short programs :). Code size does matter for instruction cache. In my application in particular, post hoc binary patching, a single byte can make a big difference in difficulty of patching.
64.
by philzook 3y ago
VLIW is what the Unison project (the context behind this post) was attacking. https://unison-code.github.io/ My best understanding is that exposing the details of the CPU to the compiler via a more complex ISA has not worke
65.
by philzook 3y ago
I think one of the biggest problems is even stating what the solution an optimal compiler would be. How does one model a program or a CPU? There almost certainly isn't one perfect model for all situations. CPU's are extremely comp
66.
Compiling with Constraints(philipzucker.com)
126 points by philzook 3y ago|36 comments
67.
Copy and Micropatch: Writing Binary Patches in C with Clang Preserve_none(philipzucker.com)
3 points by philzook 3y ago|0 comments
68.
by philzook 3y ago
Your boss either doesn't pay as much attention as you think or you should consider getting a new boss if possible. Life is too short to not indulge on curiosity.
69.
by philzook 3y ago
You can without too much work transpile datalog to SQL. SQL does have such strong support that it is useful https://github.com/philzook58/snakelog or perhaps just do it manually https://www.philipzucker.com&
70.
by philzook 3y ago
This perhaps isn't what you're asking about, but a very useful thing to realize is that datalog or sql are quite useful for subgraph isomorphims aka graph patterm matching. One can compile the graph you're looking for into th
71.
by philzook 3y ago
https://github.com/diffblue/cbmc/issues/7732 I'll note that some form of undefined behavior checking / documentation is on the roadmap for the next major version
72.
by philzook 3y ago
https://github.com/diffblue/cbmc The github repo is active and they are very responsive to issues. As you say, it is unneccesary and probably undesirable to post an issue for a tool you don't use. The links for th
73.
by philzook 3y ago
ooooooh. link? What do you mean by standardizing on hardware and toolchain? I am currently choosing ghidra and cbmc, and it seems like the approach is applicable to any compiler or arch that ghidra supports without too much change. I have o
74.
by philzook 3y ago
This is actually one of the reasons I've been tinkering with CBMC https://www.philipzucker.com/pcode2c/ The idea is to use Ghidra to lift a specialized C interpreter of the machine code and then compare to source
75.
by philzook 3y ago
Yes, correct. It does not and could not _actually_ run all possible executions unless the program state space is quite small. But from a user's perspective, it is similar. I have tried this pedagogical approach to describing verifiers
76.
by philzook 3y ago
I would love to hear more
77.
by philzook 3y ago
Yes, it returned the same "FAILURE" along with a couple new checks about getc that do pass.
78.
by philzook 3y ago
I apologize for using the word subtle. What I should have said is I don't understand the topic and reading about it has left me a sense that one should be very careful.
79.
by philzook 3y ago
Yes, I do not trust my understanding of C. Which is why I want mechanized assistance.
80.
by philzook 3y ago
For undefined behavior detection, I have heard of these: - UB sanitizer https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html - Cerberus Semantics https://www.cl.cam.ac.uk/~pes20/cerberus&#x2
81.
by philzook 3y ago
I see the calling an undefined prototype style more often, perhaps for this reason. You are probably right this is undefined behavior, but it's subtle. https://stackoverflow.com/questions/11962457/why-is-usin
82.
by philzook 3y ago
Your example does not pass the verifier cbmc /tmp/walter.c --bounds-check --pointer-check --function test ... [get.pointer_dereference.5] line 3 dereference failure: pointer outside object bounds in buffer[(signed long
83.
by philzook 3y ago
Frama-C is also very cool. Also Coq VST and however seL4 does it. I think out of all of these, CBMC requires the least expertise / has highest automation. I also don't see how it can scale beyond the unit test level, or patch toge
84.
by philzook 3y ago
Non trivial example projects https://model-checking.github.io/cbmc-training/projects.html Some crypto, AWS common C, FreeRTOS. Other interesting applications https://www.cprover.org/cbmc/applicatio
85.
The C bounded model checker: criminally underused(philipzucker.com)
209 points by philzook 3y ago|125 comments
86.
by philzook 3y ago
You might find this work and talks on liballocs by Stephen Kell interesting. The pitch is how to enable smalltalk like reflection for unix as it exists today. https://www.humprog.org/~stephen/#works-in-progress
87.
by philzook 3y ago
One of the easiest to get started on Datalog in my opinion is really clingo https://potassco.org/clingo/ , which can be pip installed and has python bindings. Answer Set Programming goes beyond datalog, but it holds da
88.
by philzook 3y ago
You might enjoy ruler https://github.com/uwplse/ruler It would be very interesting for SMT and CAS to converge a bit more. SMT in expressiveness and domains and CAS in rigor. The modality of their usage is different. C
89.
by philzook 3y ago
The herbie project using egraphs to explore different ways of rewriting floating point expressions. https://herbie.uwplse.org/ One can also write custom rulesets in egglog (a new egraph rewriting system / language &#x2
90.
by philzook 3y ago
Excellent link. I would love to see a CDCL implementation in a 100 (understandable) lines. From what I see in the repo, creusat is probably more like 1000?

More ›