Fix runtime checks #12
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Previously, when we created a monomorphic instance, we did not generate a function prototype. This caused problems for the downstream backends that then had to generate C function prototypes from function definitions which often resulted in duplicate function prototypes. This change generates the missing prototype which will allow the backends to be simplified. Signed-off-by: Alastair Reid <[email protected]>
In the past, we treated the Prelude differently from user-written code by not generating function prototypes for functions defined in the Prelude. This restriction is no longer needed and it was causing problems in the backend where we could not rely on the existence of a function prototype for every function. This change ensures that we generate function prototypes for all functions that have a FunDefn. Signed-off-by: Alastair Reid <[email protected]>
This minor simplification in all the backends generates cleaner C code by relying on earlier passes to have generated function prototypes. Signed-off-by: Alastair Reid <[email protected]>
This provides a way to perform an assertion in the middle
of an expression.
If condition e1 is TRUE, the result is e2.
If the condition e1 is FALSE, an assertion failure is reported.
This is intended for use in transformations and, in particular,
for performing runtime checks such as
x[i]
-->
__assert (i IN {0..31}) __in x[i]
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
- We need 4 locations. Signed-off-by: Alastair Reid <[email protected]>
- More usage using masks. Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
- Extends typechecker to insert runtime checks: - All 4 variants of bitslice indexing (reads and writes) - Array indexing (reads and writes) - Division by zero (Checking exact division is not done because that breaks specs that still expect DIV to mean inexact division) - Adds a disable flag to avoid insertion of runtime checks Intended to make it easier to update the ASLi version without having to fix all the runtime failures immediately. - Disables runtime checking in some testsuites where the runtime checks would overwhelm whatever we were originally trying to test. - Adds lit tests that the checks are being inserted. Signed-off-by: Alastair Reid <[email protected]>
These tests confirm that errors are being caught at runtime Signed-off-by: Alastair Reid <[email protected]>
This adds the option of using the C++ annotation 'const &'
on wide function arguments.
More specifically, this affects
bits(N) if N > limit
records
It does not affect
integer
__sint(N)
boolean
string
(But it would be easy to change each of these choices)
Signed-off-by: Alastair Reid <[email protected]>
The original exception check was a bit approximate. It would report that a function could throw an exception even if the function caught all exceptions safely. The newer exception check that is based on exception markers is much more accurate and avoids those false positives. This change disables the original check when we are using the new exception check to avoid those false positives. Signed-off-by: Alastair Reid <[email protected]>
The tests were being built with exception marker checking off which, inevitably meant that exception markers were incorrect in some places. Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
This adds a new runtime system based on the System-C library. This library gives a significant performance benefit when using hardware model checkers. Note that this adds an additional submodule dependency. Signed-off-by: Rafael Barbalho <[email protected]> Signed-off-by: Alastair Reid <[email protected]>
The C++ backends (ac & sc) can handle the bitslice accesses directly. Signed-off-by: Alastair Reid <[email protected]>
When constraints were added to the ASL language, they initially said that
in a mutable variable declaration like this
var x = 0;
the type of x is "integer {0}".
This is because the type of "0" is "integer {0}".
But this makes no sense at all - the whole point of a *mutable* variable
is that you can assign it a value that is different from the
initial value.
This change corrects this weirdness by giving x the type "integer".
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
In particular: - bitwidths - array sizes - array indexes - bitslice indexes Signed-off-by: Alastair Reid <[email protected]>
The backend/runtimes now special case the use of indexes of the form "asl_cvt_sintN_int(ix)" so we need tests for these cases. Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
Signed-off-by: Alastair Reid <[email protected]>
A long time ago, we renamed runtime_error to ASL_runtime_error but we added a backwards compatibility shim to avoid breaking code. The time has come to remove this since C++ stdlib has a conflicting name
alastairreid
force-pushed
the
areid-fix-runtime-checks
branch
from
48f1dd8 to
4215bf6
Compare
Signed-off-by: Alastair Reid <[email protected]>
This fixes a problem where constraint checks were failing because of interference between the inserted checks and the handling of expressions of the form '(a DIV b) * b == a'. Signed-off-by: Alastair Reid <[email protected]>
alastairreid
force-pushed
the
areid-fix-runtime-checks
branch
from
4215bf6 to
5d0d4a5
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This fixes a problem where constraint checks were failing because
of interference between the inserted checks and the handling of
expressions of the form '(a DIV b) * b == a'.
Also reduces the verbosity of running the test suite.