adding more checkers

[allrob23]

Hey there,

We’re working on a research project in runtime verification and have built a set of checkers that we thought might be useful for DyLin. This PR adds 19 new checkers. The description of each checker is available as a comment at the top of its file.

Let me know what you think. I'm Happy to tweak anything if needed!

[AryazE]

Thanks a lot for these interesting checkers.
Could you please add some examples to tests? The structure is that for each checker there is a directory, with one python file, and a txt file.
The txt file specifies the checkers to run, and the python file contains the example. It would be great if you could add both a code without the issue, and in the same file some code with the issue. The line that the checker should warn about is specified by a comment (you can look at some examples from other checkers in the tests directory).
I would really appreciate it, as it would also help me understand what each checker is supposed to do.

[allrob23]

Hi @AryazE, I’ve added tests for all checkers. However, there are 7 checkers I couldn’t get to run successfully:

1. Console_CloseErrorWriter and Console_CloseWriter: These cause the test suite to crash in CI because they close the writer, which terminates the output stream.
2. Thread_OverrideRun, CreateWidgetOnSameFrameCanvas, NLTK_RegexpTokenizerCapturingParentheses, Console_CloseReader, and PyDocs_MustOnlyAddSynchronizableDataToSharedList. These are failing for different reasons, but I couldn't figure out the cause yet.

Let me know if you have any ideas—happy to look into it!

[Copilot]

Pull Request Overview

Adds 19 new runtime verification checkers to DyLin, each registered in select_checkers.py and implemented as its own analysis class with a top-of-file spec comment. Key changes:

• Registration of checkers TE-02 through TE-20 in select_checkers.py
• New analyses covering sockets, threading, collections, console I/O, NLTK, random, and HTTP file handling
• Individual pre_call implementations enforcing runtime specs (e.g., non-negative timeouts, comparability, file mode)

Reviewed Changes

Copilot reviewed 58 out of 58 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
src/dylin/select_checkers.py	Adds entries TE-02 to TE-20 for the new checkers
src/dylin/analyses/Arrays_Comparable.py	New analysis to check list element comparability before sorting
src/dylin/analyses/Sets_Comparable.py	New analysis to check set element comparability before sorting
src/dylin/analyses/Console_CloseWriter.py	Warns on close() invoked on sys.stdout
src/dylin/analyses/Console_CloseReader.py	Warns on close() invoked on sys.stdin
src/dylin/analyses/Console_CloseErrorWriter.py	Warns on close() invoked on sys.stderr
src/dylin/analyses/CreateWidgetOnSameFrameCanvas.py	Ensures a widget is added to the same canvas as its frame
src/dylin/analyses/HostnamesTerminatesWithSlash.py	Checks that mount URLs terminate with a slash
src/dylin/analyses/NLTK_regexp_span_tokenize.py	Verifies the regex passed to regexp_span_tokenize isn’t empty
src/dylin/analyses/NLTK_RegexpTokenizerCapturingParentheses.py	Ensures NLTK “RegexpTokenizer” patterns use non-capturing groups
src/dylin/analyses/PriorityQueue_NonComparable.py	Flags non-comparable objects being added to a priority queue
src/dylin/analyses/PyDocs_MustOnlyAddSynchronizableDataToSharedList.py	Validates that only synchronizable data is appended to shared lists
src/dylin/analyses/RandomParams_NoPositives.py	Validates parameters for lognormvariate and vonmisesvariate
src/dylin/analyses/RandomRandrange_MustNotUseKwargs.py	Warns against keyword args in random.randrange
src/dylin/analyses/Requests_DataMustOpenInBinary.py	Enforces binary mode file opening in requests.api.post
src/dylin/analyses/Session_DataMustOpenInBinary.py	Enforces binary mode file opening in Session.post
src/dylin/analyses/socket_create_connection.py	Checks non-negative timeout in socket.create_connection
src/dylin/analyses/socket_setdefaulttimeout.py	Checks non-negative timeout in socket.setdefaulttimeout
src/dylin/analyses/socket_socket_settimeout.py	Checks non-negative timeout in socket.settimeout
src/dylin/analyses/Thread_OverrideRun.py	Flags when Thread.run isn’t overridden or no target provided

Comments suppressed due to low confidence (1)

src/dylin/analyses/RandomParams_NoPositives.py:66

• [nitpick] The error message is generic. Including the specific function name and parameter (e.g., 'sigma <= 0' or 'kappa < 0') will help users quickly identify the violating call.

f"The call to method lognormvariate or vonmisesvariate in file at {dyn_ast} does not have the correct parameters."

[Copilot]

The helper is_synchronizable never returns True for types not explicitly excluded, so valid data is flagged as unsynchronizable. Add a default return True at the end of the function.

[Copilot]

Calling getsource on a built-in or C-implemented method can raise an exception. Consider wrapping this in try/except or using a fallback to avoid runtime errors during analysis initialization.

Suggested change

	self.original_run_method_hash = sha256(getsource(threading.Thread.run).encode()).hexdigest()
	try:
	source_code = getsource(threading.Thread.run)
	self.original_run_method_hash = sha256(source_code.encode()).hexdigest()
	except Exception as e:
	# Fallback: Log a warning and set a default value
	print(f"Warning: Unable to retrieve source code for threading.Thread.run. Exception: {e}")
	self.original_run_method_hash = None

[Copilot]

[nitpick] This block adds many new entries; consider sorting or grouping the checkers logically (e.g., by category) for easier navigation and maintenance.

[AryazE]

I think we can move most of the checkers to either the "Standard Library" category (SL-*) or the "Programming Constructs" (PC-*). The rest could remain uncategorized until we have something for them.

[AryazE]

Thanks a lot for the tests, they look very good. Now I have a better understanding of what each checker is looking for.
Could you also address the comments by copilot?

I am a bit unsure about adding the checkers that raise exceptions during runtime. Since DyLin is a dynamic linter, and we need to execute the code to find the issues, the Python interpreter already warns about these errors at the correct location, which makes these checkers redundant.
My suggestion is to remove them, but let me know what you think.

Thanks again for the nice contribution!

[AryazE]

I'm also curious about how you came up with these checkers.

[allrob23]

Thanks. glad to hear the checkers were helpful!

We developed them as part of an ongoing research project and will share more details once the work is published.

I’ll address the points you raised above shortly.

[allrob23]

Hi @AryazE, I've addressed all the copilot comments and removed all the checkers that python already handles. However, the following are still failing for the following reasons:

CreateWidgetOnSameFrameCanvas -> There is no display device in the CI.
NLTK_RegexpTokenizerCapturingParentheses -> same as above.
PyDocs_MustOnlyAddSynchronizableDataToSharedList -> We will debug further to understand why it's failing.
Console_CloseWriter ->  because the test closes the stdout which is needed for the rest of the test suite.
Console_CloseErrorWriter -> same as above.

We're happy to discuss these more if needed

[AryazE]

The changes look good to me.
To avoid the issues you mentioned and move forward faster, I suggest to remove the problematic ones from this PR, and we can open another PR for them to work on those. They might need some changes to the testing harness (the CloseWriter checkers specifically).
Thanks

[allrob23]

I removed all specs with broken tests, now all tests are passing.

[AryazE]

LGTM! Thanks!