Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Specs for java.lang.System, java.lang.Integer, java.lang.Float, java.util.concurrent.atomic.AtomicBoolean/Integer/Long/Reference + Minor improvements to java.util.ArrayList, java.util.LinkedList #21

Merged
merged 95 commits into from
Dec 12, 2023
Merged
Show file tree
Hide file tree
Changes from 93 commits
Commits
Show all changes
95 commits
Select commit Hold shift + click to select a range
b3bbf6d
Fixed `indexOf` and `lastIndexOf` methods in `ArrayList` and `LinkedL…
dog-m Sep 16, 2023
49fb61a
Added implementation for `ArrayList.SubList.ListIterator`
dog-m Sep 21, 2023
abe7c53
Merge branch 'main' into patches-mikhail
dog-m Sep 23, 2023
a745ad9
Fixed variable access in `HashSet.Spliterator`
dog-m Sep 23, 2023
2905a16
Added draft implementation for `java.lang.SecurityManager` + More typ…
dog-m Sep 25, 2023
85da62a
Improvements to `SecurityManager` + More type declarations
dog-m Sep 26, 2023
5a4175c
Improvements to `SecurityManager`
dog-m Sep 26, 2023
bf4bfea
Fixed conflict during `HASHSET_VALUE` initialization
dog-m Sep 26, 2023
e80bd84
Added `java.lang.Integer` + Minor improvements to `SecurityManager`
dog-m Sep 27, 2023
139e4cc
Minor corrections to `Throwable` "implementation"
dog-m Sep 27, 2023
b9a0edb
Minor formatting improvement to `SecurityManager`
dog-m Sep 29, 2023
93a92bd
Merge branch 'actions-n-interfaces' into patches-mikhail
dog-m Sep 29, 2023
b76cc66
Merge branch 'actions-n-interfaces' into patches-mikhail
dog-m Sep 29, 2023
07ae9a8
Import cleanup
dog-m Sep 29, 2023
77b5ca9
Added basic implementation for `ArrayList.SubList#clear` method + Rem…
dog-m Sep 30, 2023
9bb4c13
Added implementation to `removeAll` and `replaceAll` methods in `Arra…
dog-m Sep 30, 2023
0ae960d
Added implementation for `ArrayList.SubList#removeAll` + Minor improv…
dog-m Oct 2, 2023
18bc5c8
Merge branch 'main' into patches-mikhail
dog-m Oct 3, 2023
f885e32
Merge branch 'main' into patches-mikhail
dog-m Oct 3, 2023
0d8d072
Improvements to element-removal-focused methods in `ArrayList` and it…
dog-m Oct 7, 2023
4bf6e4c
Merge branch 'StringBuffer-fix' into patches-mikhail
dog-m Oct 7, 2023
7429fdd
Added basic implementations for `InputStream` and `OutputStream` "nul…
dog-m Oct 8, 2023
4757e3e
Added ignore rule for IntelliJ-Idea project files
dog-m Oct 9, 2023
99f93f2
Merge branch 'StringBuffer-fix' into patches-mikhail
dog-m Oct 11, 2023
4e46c5a
Minor import adjustments + Name changes for `VoidInput(Output)Stream`
dog-m Oct 11, 2023
d1adf1e
Added lost spec for `Integer`
dog-m Oct 12, 2023
40ad85b
Added very basic implementations for some `System` methods and standa…
dog-m Oct 12, 2023
ccc487b
Added draft implementation for a "symbolic" `InputStream` + Relocatin…
dog-m Oct 14, 2023
331b0da
Minor improvements to `SymbolicInputStream`
dog-m Oct 15, 2023
21a4301
Using `SymbolicInputStream` as standard input for `System`
dog-m Oct 17, 2023
a86a612
Merge branch 'main' into patches-mikhail
dog-m Oct 17, 2023
116d736
Fix build for `Integer`
dog-m Oct 18, 2023
159edbf
Merge branch 'main' into patches-mikhail
dog-m Oct 19, 2023
fb327b2
Minor improvements to `System` and `LinkedList`
dog-m Oct 21, 2023
e070faf
Merge branch 'StringBuffer-fix' into patches-mikhail
dog-m Oct 21, 2023
725c2b0
Merge branch 'main' into patches-mikhail
dog-m Oct 26, 2023
f1c3ed1
Merge branch 'main' into patches-mikhail
dog-m Oct 27, 2023
ce813d9
Fixed incorrect operation order in `LinkedList#set` method
dog-m Oct 28, 2023
a57681d
Simplified sorting within `ArrayList` and `LinkedList` (and sublists)…
dog-m Oct 29, 2023
8208f07
Improved `System` IO + Improvements to `LinkedList` + Added `java.uti…
dog-m Oct 30, 2023
e3cdf1b
Enabled back `System.err` initialization + Disabled `BufferedInputStr…
dog-m Oct 31, 2023
b8dd86c
Added implementation for `AtomicBoolean`
dog-m Nov 2, 2023
7aeddc7
Added implementation for `AtomicInteger`
dog-m Nov 3, 2023
6289ca5
Minor formatting changes for `System#in`
dog-m Nov 3, 2023
842453f
Merge branch 'main' into patches-mikhail
dog-m Nov 3, 2023
44cb3a7
Added `AtomicLong` + Minor simplifications for `AtomicInteger` and `A…
dog-m Nov 3, 2023
a77550c
Added implementation for `AtomicReference` + Minor comment fixes for …
dog-m Nov 3, 2023
a893a4b
Removed redundant annotation for `AtomicReference`
dog-m Nov 3, 2023
4920b6f
Minor improvements to `System` + Barebones declaration for `VM` and `…
dog-m Nov 5, 2023
d5dd7ec
Prepared `Charset` approximation skeleton for the translator + Added …
dog-m Nov 7, 2023
3ef1c15
Corrections for experimental type conversion
dog-m Nov 8, 2023
2f191d3
Temporarily disabled error initialization in `System::initPhase1` due…
dog-m Nov 8, 2023
2330c8e
Merge branch 'main' into patches-mikhail
dog-m Nov 9, 2023
2a47a5b
Improvements to `System`
dog-m Nov 9, 2023
f4319e8
Minor fixes to `System`
dog-m Nov 9, 2023
a067c80
Added basic collection of properties within `System`
dog-m Nov 10, 2023
db75b85
Added symbolic string construction utils to `Stream`
dog-m Nov 10, 2023
1c12c37
Minor property-focused fixes within `System`
dog-m Nov 10, 2023
25684a4
Simplification for some properties in `System`
dog-m Nov 10, 2023
30f6fbd
Improvements and implementations for `java.lang.Integer`
dog-m Nov 12, 2023
f0f8b08
Disabled synthesis for `Charset` + Added approximation for `Float` (a…
dog-m Nov 12, 2023
c4a6e57
Improvements to `Float` and `Integer`
dog-m Nov 13, 2023
ec9e387
Minor fixes for `Float`
dog-m Nov 13, 2023
5dc83f1
Fixed incorrect package name for `Stream` spliterators
dog-m Nov 14, 2023
a0d94df
Added implementation for `java.lang.Double`
dog-m Nov 14, 2023
f03947b
Added action `TYPE_OF`
dog-m Nov 15, 2023
e64603c
Added missing declaration for `@abstract` annotation + Added static m…
dog-m Nov 15, 2023
dd3f7ef
Minor improvements to `double/float` to `long/int` conversion modelling
dog-m Nov 22, 2023
ea07983
Minor field access optimization for `java.lang.System`
dog-m Nov 23, 2023
fe5b76f
Fix some issues found by the reviewer
dog-m Nov 24, 2023
5992719
Micro-optimization for `java.lang.System`: reduced access to static v…
dog-m Nov 25, 2023
3285a0c
Added alternative initialization for `java.lang.System` + Minor impro…
dog-m Nov 27, 2023
55f4ce3
Removed `length` automaton variable for `java.util.ArrayList`
dog-m Nov 28, 2023
ce0abda
Merge branch 'main' into patches-mikhail
dog-m Nov 29, 2023
793d55c
Removed `length` automaton variable from `HashSetAutomaton` + Minor i…
dog-m Nov 29, 2023
da47634
Removed `length` variable from `LinkedHashSetAutomaton` + Minor impro…
dog-m Nov 29, 2023
d6589de
Spec file rename
dog-m Nov 29, 2023
6009330
Removed `size` variable from `LinkedListAutomaton` + Minor improvements
dog-m Nov 29, 2023
565f4ef
Merge branch 'main' into patches-mikhail
dog-m Nov 29, 2023
183b705
Activated custom stream implementations for some collections
dog-m Nov 29, 2023
6b347fd
Package name change for utility automata and types
dog-m Nov 29, 2023
62389e9
Merge branch 'main' into patches-mikhail
dog-m Nov 30, 2023
658b7d5
MInor improvements to `java.lang.StringBuffer/StringBuilder` and `jav…
dog-m Nov 30, 2023
dc43f12
Added missing `ArrayList`-based implementations for `java.util.Linked…
dog-m Nov 30, 2023
ca777fb
Fixed subroutine parameter not being used
dog-m Nov 30, 2023
33481b6
Fixed `toString` method for `java.util.HashSet/LinkedHashSet` + Made …
dog-m Nov 30, 2023
cef0411
Failed attempts to improve `java.security.SecureRandom`
dog-m Dec 6, 2023
ebfd88b
Moved array-based spliterators into `java.util.*` package + Added typ…
dog-m Dec 8, 2023
75c9b65
Added partial implementation for `java.util.Spliterators` + Added imp…
dog-m Dec 9, 2023
98fac71
Switched `java.util.stream.Stream` implementation from custom spliter…
dog-m Dec 10, 2023
0246b2d
Minor improvements to `java.security.SecureRandom`
dog-m Dec 10, 2023
73d8326
Corrections to function names
dog-m Dec 11, 2023
b9463ee
Added implementation to `java.lang.Object#clone` method
dog-m Dec 11, 2023
6c787b0
Fixed a typo in class name
dog-m Dec 12, 2023
db77c7d
Improved `java.lang.Object#clone` method
dog-m Dec 12, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions spec/java.common.lsl
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,8 @@ annotation packageprivate ();

annotation public ();

annotation abstract ();

annotation extends (
canonicalClassName: string,
);
Expand Down
27 changes: 27 additions & 0 deletions spec/java/io/Console.lsl
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
//#! pragma: non-synthesizable
libsl "1.1.0";

library std
version "11"
language "Java"
url "https://github.com/openjdk/jdk11/blob/master/src/java.base/share/classes/java/io/Console.java";

// imports

import java/io/Flushable;


// primary semantic types

@final type Console
is java.io.Console
for Flushable
{
}

// see java.io.Console#istty
val CONSOLE_IS_TTY: boolean = action SYMBOLIC("boolean");
alexeev509 marked this conversation as resolved.
Show resolved Hide resolved


// global aliases and type overrides

24 changes: 24 additions & 0 deletions spec/java/io/FileDescriptor.lsl
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
//#! pragma: non-synthesizable
libsl "1.1.0";

library std
version "11"
language "Java"
url "https://github.com/openjdk/jdk11/blob/master/src/java.base/share/classes/java/io/FileDescriptor.java";

// imports

import java/lang/Object;


// primary semantic types

@public type FileDescriptor
is java.io.FileDescriptor
for Object
{
fun valid(): boolean;

@throws(["java.io.SyncFailedException"])
fun sync(): void;
}
3 changes: 2 additions & 1 deletion spec/java/lang/Byte.lsl
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,9 @@ import java/lang/Number;
@FunctionalInterface("byteValue")
@final type Byte
is java.lang.Byte
for Comparable, Number, byte
for Comparable, Number
{
// WARNING: use 'byteValue' to get primitive value
}


Expand Down
7 changes: 5 additions & 2 deletions spec/java/lang/Character.lsl
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ library std
// imports

import java/io/Serializable;
import java/lang/CharSequence;
import java/lang/Comparable;


Expand All @@ -17,11 +18,13 @@ import java/lang/Comparable;
@FunctionalInterface("charValue")
@final type Character
is java.lang.Character
for Comparable, Serializable, char
for Comparable, Serializable
{
// WARNING: use 'charValue' to get primitive value

fun *.charValue(): char;

@static fun offsetByCodePoints(seq: CharSequence, index: int, codePointOffset: int): int;
@static fun *.offsetByCodePoints(seq: CharSequence, index: int, codePointOffset: int): int;
}


Expand Down
24 changes: 24 additions & 0 deletions spec/java/lang/ClassLoader.lsl
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
//#! pragma: non-synthesizable
libsl "1.1.0";

library std
version "11"
language "Java"
url "https://github.com/openjdk/jdk11/blob/master/src/java.base/share/classes/java/lang/ClassLoader.java";

// imports

import java/lang/Object;


// primary semantic types

@final type ClassLoader
is java.lang.ClassLoader
for Object
{
}


// global aliases and type overrides

41 changes: 36 additions & 5 deletions spec/java/lang/Double.lsl
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ library std
// imports

import java/lang/Comparable;
import java/lang/Class;
import java/lang/Number;


Expand All @@ -17,14 +18,44 @@ import java/lang/Number;
@FunctionalInterface("doubleValue")
@final type Double
is java.lang.Double
for Comparable, Number, double
for Comparable, Number
{
}
// WARNING: use 'doubleValue' to get primitive value

@static fun *.isNaN(x: double): boolean;

val DOUBLE_POSITIVE_INFINITY: double = 1.0 / 0.0;
val DOUBLE_NEGATIVE_INFINITY: double = -1.0 / 0.0;
val DOUBLE_NAN: double = 0.0 / 0.0;
@static fun *.isFinite(x: double): boolean;
@static fun *.isInfinite(x: double): boolean;

@static fun *.valueOf(x: double): Number; // #problem: self-reference
}


// global aliases and type overrides

@extends("java.lang.Number")
@implements("java.lang.Comparable<Double>")
@final type LSLDouble
is java.lang.Double
for Double
{
@private @static val serialVersionUID: long = -9172774392245257468L;

@static val BYTES: int = 8;
@static val SIZE: int = 64;

@static val MAX_EXPONENT: int = 1023;
@static val MIN_EXPONENT: int = -1022;

// #problem: no support for scientific notation
@static val MAX_VALUE: double = action DEBUG_DO("1.7976931348623157E308");
@static val MIN_VALUE: double = action DEBUG_DO("4.9E-324");
@static val MIN_NORMAL: double = action DEBUG_DO("2.2250738585072014E-308");

@static val POSITIVE_INFINITY: double = 1.0 / 0.0;
@static val NEGATIVE_INFINITY: double = -1.0 / 0.0;

@static val NaN: double = 0.0 / 0.0;

@static val TYPE: Class = action TYPE_OF("Double");
}
Loading