Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Apr 05 20:47
    MiroFurtado starred pschanely/CrossHair
  • Apr 05 20:17
    hanhanhan starred pschanely/CrossHair
  • Apr 05 17:17

    pschanely on master

    Implemented collections deque (… (compare)

  • Apr 05 17:17
    pschanely closed #13
  • Apr 05 17:16
    pschanely commented #13
  • Apr 05 12:59
    pschanely labeled #28
  • Apr 05 12:55
    pschanely opened #28
  • Apr 04 20:02
    abe-winter starred pschanely/CrossHair
  • Apr 04 16:31

    pschanely on master

    Add a deferred uniqueness check… (compare)

  • Apr 04 08:29
    pschanely commented #22
  • Apr 04 01:36
    Zac-HD labeled #27
  • Apr 04 01:36
    Zac-HD opened #27
  • Apr 03 22:41
    pschanely closed #4
  • Apr 03 22:41
    pschanely commented #4
  • Apr 03 22:39

    pschanely on master

    Add TODO test for date arithmet… (compare)

  • Apr 02 03:16

    pschanely on master

    Add symbolic patches and regist… (compare)

  • Apr 01 13:22

    pschanely on master

    Framework for deferring assumpt… Defer date validation. (compare)

  • Apr 01 04:06
    leplatrem starred pschanely/CrossHair
  • Apr 01 03:43
    GraceFatima commented on af35039
Tejas Shetty
@TejasAvinashShetty
hi
Phillip Schanely
@pschanely
Hey friends! Don't be shy with the questions/comments/musings.
oneEdoubleD
@oneEdoubleD
Hey @pschanely :) I'm Edd, the guy who emailed you from HN. What are the next things you're looking at implementing? I could start contributing this weekend :)
Phillip Schanely
@pschanely
@oneEdoubleD An good starter thing (but perhaps not terribly interesting?) is stuff like this pschanely/CrossHair#3 - generally speaking, CrossHair cannot deal with types implemented in C (like collections.deque), so there is a pattern where we implement some of the standard library in terms of other types that we do symbolically implement. So, for example, if you were to implement deque in terms of native python lists (which would be horribly inefficient in normal execution), we could then use such a class when someone wants to analyze a function with a deque argument. I'd like to do some refactoring today to make this pattern a little more clear, but could be ready for poking at this weekend if it looks interesting to you!
oneEdoubleD
@oneEdoubleD
Sure sounds good!
Ping me when you've pushed the refactor and I'll take a look then :)
Phillip Schanely
@pschanely
Roger; will ping you soon! Very exciting!
oneEdoubleD
@oneEdoubleD

Are there any other steps to run CrossHair except for the two steps mentioned in the readme file? I'm trying to run Master at the moment.

pip install git+https://github.com/pschanely/crosshair
crosshair watch <directory>

Is throwing a ModuleNotFoundError about crosshair.libimpl.

(base) C:\Users\hey\Github\crosshair>crosshair
Traceback (most recent call last):
  File "c:\users\hey\anaconda3\lib\runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  File "c:\users\hey\anaconda3\lib\runpy.py", line 85, in _run_code
    exec(code, run_globals)
  File "C:\Users\hey\Anaconda3\Scripts\crosshair.exe\__main__.py", line 5, in <module>
  File "c:\users\hey\anaconda3\lib\site-packages\crosshair\main.py", line 26, in <module>
    from crosshair.libimpl import make_registrations
ModuleNotFoundError: No module named 'crosshair.libimpl'
(Side note, code markup in Gitter is so much nicer than Slack!)
Phillip Schanely
@pschanely
Hmm; let me try this on a windows machine shortly - haven't attempted that yet. If you are doing development, you probably want a slightly different setup which might or might not work around the issue you're currently having: enter a new conda environment, clone the repository, cd into the root of the repository, and run python setup.py develop and then try crosshair watch
Phillip Schanely
@pschanely
Another thing you could try is setting your PYTHONPATH to the repo root and running python crosshair/main.py watch <DIR>.
That should be the same thing as the crosshair command.
Also, an update: I might not be able to get access to a windows box until next week - the one I thought I might be able to use now is pretty locked down. :( I bet it's something with the console_scripts stuff in setup.py
And, finally, if you take that manual approach, you need to manually install (with pip) the dependencies listed in setup.py too.
Phillip Schanely
@pschanely
Nevermind! I think I know what this issue is and can fix it quickly
Phillip Schanely
@pschanely
Done. Please try again and let me know how it goes!
oneEdoubleD
@oneEdoubleD
Yep, that's working now! Thanks :)
oneEdoubleD
@oneEdoubleD
Are we essentially implementing our own ListBasedDeque over a list but offering the same functionality as https://docs.python.org/3/library/collections.html#collections.deque?
For example something like this?
T = TypeVar('T')
class ListBasedDeque:
    def __init__(self, contents: List[T], maxlen: Optional[int]=None):
        self._contents = contents
        self._maxlen = maxlen

    def _has_room(self) -> bool:
        maxlen = self._maxlen
        return maxlen is None or len(self._contents) < maxlen

    def appendleft(self, item: T):
        if self._has_room():
            self._contents = [item] + self._contents

    def append(self, item: T):
        if self._has_room():
            self._contents = self._contents + [item]

    def clear(self):
        self._contents = []

    def count(self, item: T):
        count = 0
        for i in self._contents:
            if i == item:
                count += 1
        return count

    def index(self, item :T):
        pass

    def insert(self, item: T):
        pass

    def pop(self):
        x = self._contents[-1]
        del self._contents[-1]
        return x

    def popleft(self):
        x = self._contents[0]
        del self._contents[0]
        return x

    def remove(self, item: T):
        self._contents.remove(item)

    def reverse(self):
        self._contents.reverse()

    def rotate(self, n=1):
        steps = 0
        if n >= 0:
            while steps <= n:
                self.appendleft(self.pop())
                steps += 1
        if n < 0:
            while steps >= n:
                self.append(self.popleft())
                steps -= 1

    def maxlen(self):
        return self._maxlen
(Mostly untested, pretty sure rotate and reverse are broken)
Phillip Schanely
@pschanely
Yup - you've got the right idea! For every C-based type, we implement a type that pretends to be it: we can choose to either implement it (1) using z3 directly, or (2) implement it using other types that are already have implementations in z3. Usually option 2 is easier/less error prone if it is available. In the test file, I started a few tests that confirm that crosshair understands the deque type, but you'll want to add some tests that confirm your implementation of deque works just like the real one. (which you can test without even using anything that is crosshair-specific)
There are some tricks to making crosshair work efficiently: one is that you want to avoid iterating over a list if you can. So, if you can figure out how to implement rotate() using slices, crosshair will be able to analyze calls to rotate without needing to materialize the size of the symbolic list.
oneEdoubleD
@oneEdoubleD

There are some tricks to making crosshair work efficiently: one is that you want to avoid iterating over a list if you can. So, if you can figure out how to implement rotate() using slices, crosshair will be able to analyze calls to rotate without needing to materialize the size of the symbolic list.

I might need more coffee, but append and pop are O(1) and the steps variable is just being used to keep track of the rotations - I don't think we iterate over the list at any point? I could make my code clearer if it gives that impression though!

Phillip Schanely
@pschanely
Oh, nope that's right! I think rotate() is the only one that might be able to avoid the loop. And not even positive about that.
Oh wait I see what you are saying, hold on
I was thinking something like this (but maybe have reversed?):
def rotate(self, n):
  contents = self._contents
  if n >=0:
    self._contents = contents[-n:] + contents[:-n]
  ...
oneEdoubleD
@oneEdoubleD
Ahh I see, yeah that's nicer :)
oneEdoubleD
@oneEdoubleD
@pschanely I've made a PR here - pschanely/CrossHair#13
Let me know if you'd like any additional test coverage or if I've missed anything :)
Is there a list of classes that still need this work to be done?
Phillip Schanely
@pschanely
This is so awesome. Sent a quick first round of comments.
A for even more stuff to look at, it's not hard to find similar cases as this, but I don't have a list of what's missing.
I think defaultdict is in a similar situation right now. The datetime module is also in rough shape, but our approach for that probably requires some extra thought.
Also, a PR for a contributors section of the readme please, listing you (in whatever form you like). Link your name to something too if you want :)
oneEdoubleD
@oneEdoubleD

Also, a PR for a contributors section of the readme please, listing you (in whatever form you like). Link your name to something too if you want :)

pschanely/CrossHair#14

Let me know if you'd like me to add anyone else too :)

This is so awesome. Sent a quick first round of comments.

Will get around to this probably today but maybe tomorrow - I live in Oxford so UTC time zone!

oneEdoubleD
@oneEdoubleD

Will get around to this probably today but maybe tomorrow - I live in Oxford so UTC time zone!

Lol how optimistic and foolish I was on Sunday... Work has been crazy, will finish the PR on Saturday.

Phillip Schanely
@pschanely
We aren't on a schedule! 😁
Also, I am presently trying to recruit people to try it out and file bugs. If anyone here knows someone who might, please encourage them to do so!
Phillip Schanely
@pschanely
Some updates: got a lot of interest and great feedback on lobste.rs over the weekend! https://lobste.rs/s/k5umvd/crosshair_static_analysis_tool_for
Notably, discovered the Fuzzing Book, which describes roughly the same process that CrossHair follows: https://www.fuzzingbook.org/html/SymbolicFuzzer.html#Symbolic-Fuzzing
Phillip Schanely
@pschanely
CrossHair idea of the day: Use an immutable mixin to make sure your classes stay that way! :) https://crosshair-web.org/?gist=20c2e8060c7a9b1e20080bad5f30201f
Saul Shanabrook
@saulshanabrook
Have you experimented at all with cvc4?
Phillip Schanely
@pschanely
Not yet! I've considered at points migrating to pure SMTLIB so that we could have pluggable backends, but it's quite a bit of work!
Phillip Schanely
@pschanely
@saulshanabrook saw your note on the verbose mode - you don't get something like this?:
$ crosshair check -v crosshair.examples.arith.double
| |check() Check  double
|   |analyze_function() Analyzing  double
|    |analyze_single_condition() Analyzing postcondition: " len(_) == len(items) * 2 "
|    |analyze_single_condition() assuming preconditions:  
|    |analyze_single_condition() deadline in secs: 1584896971.860963 cur: 1584896970.360966
|     |analyze_calltree() Begin analyze calltree  double
|     |analyze_calltree() time: 1584896970.572696
|     |analyze_calltree() Iteration  1
|       |gen_args() created proxy for items as type: <class 'crosshair.libimpl.builtinslib.SmtList'>
|      |attempt_call() Postcondition confirmed.
|     |analyze_calltree() Iter complete. Worst status found so far: CONFIRMED
|     |analyze_calltree() Exhausted  calltree search with CONFIRMED and 0 messages. Number of iterations:  1
Saul Shanabrook
@saulshanabrook
Yep!
I did, but when I uncommented the lines you suggested, I thought there would be more added
Phillip Schanely
@pschanely
ah
maybe i gave you the wrong line :) lemme double check
Saul Shanabrook
@saulshanabrook
Yeah it seems like that function wasn't called at all :)
Phillip Schanely
@pschanely
Saul Shanabrook
@saulshanabrook
K, thanks!
Phillip Schanely
@pschanely
@saulshanabrook Feel free to add yourself to the contributors list and link to anything you want. :)
Saul Shanabrook
@saulshanabrook
Ha thanks! :D